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.

Happy to announce four open positions for PhD candidates in our "Future of Software Engineering" (FUSE) lab!

The open positions are in the areas of code review efficiency, predictive software testing, automated code refactoring and engineering productivity metrics.

FUSE is hosted by the Software Engineering Research Group (SERG) at TU Delft. Within FUSE we collaborate with Meta's Developer Infrastructure team.

More info: https://se.ewi.tudelft.nl/fuse-lab/vacancies.html

Apply now, apply before January 4!

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 (@[email protected] 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

Hello testers! 👋

Where did you get your testing expertise from? University, college, book, on the job? Maybe somewhere else?

Please fill out our 5-10 minute survey and help advance testing research and education 🙏

https://tudelft.fra1.qualtrics.com/jfe/form/SV_5jwFDiRFhh4EABg