Sára Juhošová

My Research ▸
My Projects ▸
Personal Blog ▸
Pretty Pictures ▸
Awards of the Year ▸
sarajuhosova in/sjuhosova sarantja sarantja

Hello, World! ☀️

🧪 My Research

[Current] Type-Driven Development in Practice

in collaboration with: Jesper Cockx

As part of our research on the usability of interactive theorem provers, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in tools that encourage and facilitate type-driven development, especially in cases when they can help us reason about complex problems.

We are hoping to use your responses to identify the characteristic language features and tool interactions that enable type-driven development, with the eventual goals of enhancing them and bringing their benefits to a wider range of programmers.

You are welcome to participate if you have experience with any type-driven development tool, including dependently-typed languages (e.g., Coq, Lean, Agda), refinement types (e.g., Liquid Haskell), or even other static type systems (e.g., in Rust or Haskell).

Fill in our anonymous, 10-minute survey here!

[2025] Pinpointing the Learning Obstacles of an Interactive Theorem Prover

in collaboration with: Andy Zaidman Jesper Cockx

Interactive theorem provers (ITPs) are programming languages which allow users to reason about and verify their programs. Although they promise strong correctness guarantees and expressive type annotations which can act as code summaries, they tend to have a steep learning curve and poor usability. Unfortunately, there is only a vague understanding of the underlying causes for these problems within the research community. To pinpoint the exact usability bottlenecks of ITPs, we conducted an online survey among 41 computer science bachelor students, asking them to reflect on the experience of learning to use the Agda ITP and to list the obstacles they faced during the process. Qualitative analysis of the responses revealed confusion among the participants about the role of ITPs within software development processes as well as design choices and tool deficiencies which do not provide an adequate level of support to ITP users. To make ITPs more accessible to new users, we recommend that ITP designers look beyond the language itself and also consider its wider contexts of tooling, developer environments, and larger software development processes.

ICPC '25

Pre-Print

[2024] How Novices Perceive Interactive Theorem Provers (Extended Abstract)

Interactive theorem provers (ITPs) are known to have a steep learning curve and poor usability. This hinders their spread into commercial software development, wasting their potential to improve software quality. To understand what makes them inaccessible to novices, we conducted an online survey among bachelor students, asking them to list the obstacles they encountered while learning Agda. Analysis of the results revealed design choices and tool deficiencies which do not provide an adequate level of support to beginner nor advanced users. These observations point to one prominent point of improvement: providing a more accessible and sturdy infrastructure for ITP programmers.

ICFP SRC '24
TyDe '24

Extended Abstract TyDe Talk Poster Slides Haskell Interlude

[2023] Bringing Formal Verification into Widespread Programming Language Ecosystems (MSc Thesis)

Formal verification is a powerful tool for ensuring program correctness but is often hard to learn to use and has not yet spread into the commercial world. This thesis focuses on finding an easy-to-use solution to make formal verification available in popular programming language ecosystems. We propose a solution where users can write code in an interactive theorem prover and then transpile it into a more popular programming language. We use Agda2HS as a case study to determine what challenges users find in using such a tool, improve selected features, and then conduct a user study to evaluate the usability. We find that detailed documentation, support for commonly-used features in the target programming language, features that facilitate verification, integration of the tool into the target ecosystem, and user studies are necessary for the accessibility of such a tool.

TU Delft

Repository

🛠️ My Projects

GRaffe

icon by surang

A graph definition language

Check it out ▸

Suguru

icon by Freepik

A Jigsaw Sudoku puzzle
(a.k.a. Tectonic or Suguru)

Check it out ▸

🖋️ Personal Blog

board-games recommendations

Best Board Games

26 February 2025

Read post ▸

...or discover the posts
by category!

📷 Pretty Pictures

by me

Cliffs of Moher

County Clare, Ireland

15 July 2023

Edinburgh Castle

Edinburgh, Scotland

27 July 2024

Chata pri Zelenom plese

Vysoké Tatry, Slovakia

21 July 2021

Dunguaire Castle

Kinvarra, Ireland

15 July 2023

Sheep!

Heemskerk, The Netherlands

17 December 2022

Parc Guëll

Barcelona, Spain

01 September 2022

Modern Art

Delft, The Netherlands

03 June 2022

Metro Madness

Lisbon, Portugal

24 July 2019

Ring of Kerry

Waterville Beach, Ireland

17 July 2023

Parliament House

Budapest, Hungary

26 October 2023

Catedral de Sevilla

Seville, Spain

21 July 2019

BalPol

Delft, The Netherlands

28 May 2020

Real Alcázar de Sevilla

Seville, Spain

21 July 2019

Basílica de la Sagrada Família

Barcelona, Spain

31 August 2022

Catedral de la Almudena

Madrid, Spain

27 July 2019

Sunsets & Surfing

Moliets-et-Maa, France

09 August 2021

Giraffe!

Murchison Falls National Park, Uganda

30 December 2019

A Winding Way

Kibale National Park, Uganda

28 December 2019

🏆 Awards of the Year

a.k.a. Sára's Favourites

This is an overview of the things I enjoyed the most each year - it does not correlate with release dates nor with my all-time favourites.

  • Books  
    Brandon Sanderson - Secret (Cosmere) Projects ★★★★★

    Tress and the Emerald Sea: whimsical, adventurous, and just downright enjoyable.
    The Sunlit Man: quick-paced, unique, and startlingly memorable.
    Yumi and the Nightmare Painter: cosy, charming, and incredibly creative.

  • Board Game  
    Gaia Project ★★★★★

    What a well-designed game!

  • Video Game  
    The Witcher 3: Wild Hunt ★★★★

  • Book Series  
    Robert Jordan - The Wheel of Time ★★★★

  • Board Game  
    Clank!: A Deck-Building Adventure ★★★★

    Usually, I hate any kind of element of luck in a board game, but the way it's incorporated in Clank! makes me forgive it. The premise of this game is that you are a thief trying to steal treasures from a dragon's lair. Certain actions make you Clank!, generating noise, and making it more likely that the dragon will harm you in its next attack. This game really feels like a video game brought on the table, and it made me love deck-building as a mechanic.

  • Video Game  
    Pokémon: Shield ★★★

  • Book  
    Andy Weir - The Martian ★★★★★

    This book is probably my all-time favourite. I picked it up not knowing what to expect and was positively surprised in every aspect. The story, the characters, and the style of writing are delightful. Though there are plenty of small details to consume, the story keeps advancing and the pacing is perfect. I loved how the story felt like something that could actually happen in our world. Last but not least, this might be the only book that's actually made me laugh out loud at multiple occasions.

  • Board Game  
    Terraforming Mars ★★★★★

    This game has the perfect amount of resource competition - just enough to keep it interesting, but not enough to make you nervous. With great mechanics, ideal playtime, and a cool topic, this is probably our most played game. The only complaint I have about this game is the component quality - and you can fix that by buying the Terraforming Mars: Big Box.

  • Video Game  
    Horizon Zero Dawn ★★★★★

    I did not grow up playing video games, and this was the first I ever started, enjoyed, and played one through completely. The art is beautiful, the story is captivating, and the gameplay is fun (albeit quite difficult for someone who does not know how to operate a controller).