Jesper Agdakx 🔸<p>As part of our (@sarantja@mastodon.social and yt) research on <strong>the usability of interactive theorem provers</strong>, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in <strong>tools that encourage and facilitate type-driven development</strong>, especially in cases when they can help us reason about complex problems.</p><p>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.</p><p>Please fill in our <em>anonymous</em>, 10-minute survey here: <a href="https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS" rel="nofollow noopener noreferrer" target="_blank">https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS</a></p><p>You are welcome to participate if you have experience with <em>any</em> 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><p>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.</p><p><a class="hashtag" href="https://agda.club/tag/agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> <a class="hashtag" href="https://agda.club/tag/coq" rel="nofollow noopener noreferrer" target="_blank">#Coq</a> <a class="hashtag" href="https://agda.club/tag/rocq" rel="nofollow noopener noreferrer" target="_blank">#Rocq</a> <a class="hashtag" href="https://agda.club/tag/lean" rel="nofollow noopener noreferrer" target="_blank">#Lean</a> <a class="hashtag" href="https://agda.club/tag/liquidhaskell" rel="nofollow noopener noreferrer" target="_blank">#LiquidHaskell</a> <a class="hashtag" href="https://agda.club/tag/rust" rel="nofollow noopener noreferrer" target="_blank">#Rust</a> <a class="hashtag" href="https://agda.club/tag/haskell" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a class="hashtag" href="https://agda.club/tag/typedrivendevelopment" rel="nofollow noopener noreferrer" target="_blank">#TypeDrivenDevelopment</a> <a class="hashtag" href="https://agda.club/tag/tyde" rel="nofollow noopener noreferrer" target="_blank">#TyDe</a> <a class="hashtag" href="https://agda.club/tag/dependenttypes" rel="nofollow noopener noreferrer" target="_blank">#DependentTypes</a> <a class="hashtag" href="https://agda.club/tag/liquidtypes" rel="nofollow noopener noreferrer" target="_blank">#LiquidTypes</a> <a class="hashtag" href="https://agda.club/tag/refinementtypes" rel="nofollow noopener noreferrer" target="_blank">#RefinementTypes</a> <a class="hashtag" href="https://agda.club/tag/proofassistants" rel="nofollow noopener noreferrer" target="_blank">#ProofAssistants</a> <a class="hashtag" href="https://agda.club/tag/survey" rel="nofollow noopener noreferrer" target="_blank">#Survey</a></p>