Check out the pre-print of our latest work, accepted at ICPC'26:

"The Way of Types: A Report on Developer Experience with Type-Driven Development" by me, @azaidman, and @jesper

https://sarajuhosova.com/assets/files/2026-icpc.pdf

To determine how current practitioners experience the use of type-driven development (TyDD) and what inhibits its adoption by a wider range of developers, we conducted a survey with 130 participants from various backgrounds, asking them to describe their experience with current TyDD tools.

Master thesis by Maria Khakimova: "Enhancing Proof Assistant Error Messages with Hints: A User Study"

"We implemented hint enhancements for the error messages displayed upon three common mistakes: forgetting whitespace, using confusable Unicode characters, and supplying too few arguments to a function. A between-participants user study was then conducted with 70 students [..]"

https://repository.tudelft.nl/record/uuid:52513287-7149-41f1-a8e8-8e38696cb283

#Agda #DependentTypes #ProofAssistants #ErrorMessages #Usability #UserStudy #master #thesis

Proud to announce that our ICPC’25 paper on “Pinpointing the Learning Obstacles of an Interactive Theorem Prover” received the Distinguished Paper Award!

Huge thanks to @jesper and @azaidman for the collaboration!

The pre-print is available on my website:
https://sarajuhosova.com/assets/files/2025-icpc.pdf

As part of our (@sarantja@mastodon.social and yt) 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.

Please fill in our anonymous, 10-minute survey here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS

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).

P.S. In case you remember signing up for an interview with us in a previous survey and are now wondering whether that study will still go on, the answer is: yes! We’ve had to revise our schedule, but we are still excited to talk to you and will start inviting people for an interview soon.

#Agda #Coq #Rocq #Lean #LiquidHaskell #Rust #Haskell #TypeDrivenDevelopment #TyDe #DependentTypes #LiquidTypes #RefinementTypes #ProofAssistants #Survey

The pre-print for the #ICPC paper “Pinpointing the Learning Obstacles of an Interactive Theorem Prover” by @sarantja @azaidman and yt is now available at https://sarajuhosova.com/assets/files/2025-icpc.pdf

I very much hope this will inspire more research on the usability and accessibility of the languages we build going forward!

Abstract:

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.

#Agda #TheoremProving #DependentTypes #Usability #Accessibility #ICPC25

Extended abstract by Sára Juhošová at TyDe '24: How Novices Perceive Interactive Theorem Provers

"we conducted an online survey among bachelor students, asking them to list the obstacles they encountered while learning Agda. [...]These observations point to one prominent point of improvement: providing a more accessible and sturdy infrastructure for ITP programmers."

https://icfp24.sigplan.org/details/tyde-2024-papers/1/How-Novices-Perceive-Interactive-Theorem-Provers-Extended-Abstract-

#agda #theoremprovers #usability #tyde

My PhD student Sára and I are looking for people to participate in a study on usability aspects of interactive theorem provers. Please consider signing up!

Who? anyone who uses or has used an interactive theorem prover for whatever purpose

What? 90 - 120 minute interviews (possibly including a small think-aloud programming session)

When? interviews will be scheduled starting September 2024

Where? online (participants from anywhere are welcome)

We are hoping these interviews will help us determine how you interact with your theorem provers and to gain insights on how we can improve the user experience. We are interested in all aspects of interactive theorem provers, including but not limited to their design, their tooling, their libraries, and their documentation.

Sign up here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_0UJKuqcWC9G4FEy

#Agda #Coq #Lean #Isabelle #Usability #TheoremProvers