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

... #LiquidHaskell (restriction types, SMT solver) and the Isabelle proof assistant.

For example, look at the kind of assurances we can make about data at the type-level. This means the SMT solver can assure that certain logical constraints on types are provably true.

My code to verify a file ranking algo I made:

https://github.com/someodd/bore/blob/master/src/Bore/SpacecookieClone/Search/Verified.hs

Readings shared September 13, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/13-readings_shared_09-13-24 #Haskell #FunctionalProgramming #LiquidHaskell #Emacs #OrgMode

Reflecting away from definitions in Liquid Haskell. ~ Jonathan Arnoult. https://www.tweag.io/blog/2024-09-12-lh-reflection #Haskell #FunctionalProgramming #LiquidHaskell

Lecturas compartidas el 21 de julio de 2024. https://jaalonso.github.io/vestigium/posts/2024/07/22-lecturas_compartidas_el_21-jul-24 #ITP #IsabelleHOL #Coq #Logic #Math #FunctionalProgramming #Haskell #LiquidHaskell

Liquid amortization: Proving amortized complexity with LiquidHaskell (Functional pearl). ~ Jan van Brügge. https://arxiv.org/abs/2407.13671 #FunctionalProgramming #Haskell #LiquidHaskell

Lecturas compartidas el 18 de julio de 2024. https://jaalonso.github.io/vestigium/posts/2024/07/19-lecturas_compartidas_el_18-jul-24 #ITP #Coq #IsabelleHOL #FunctionalProgramming #Haskell #LiquidHaskell #AI #ChatGPT #Math

Modular implementation and formalization of dynamic policies (Work in progress). ~ Antonio Zegarelli, Niki Vazou, Marco Guarnieri. https://fcs-workshop.github.io/fcs2024/papers/FCS_Zegarelli_Vazou_Guarnieri.pdf #FunctionalProgramming #LiquidHaskell

Lecturas compartidas el 31 de mayo de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/01-lecturas_compartidas_el_31-may-24 #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #LiquidHaskell

Liquid Haskell through the compilers. ~ Facundo Domínguez. https://www.tweag.io/blog/2024-05-30-lh-upgrades/ #FunctionalProgramming #LiquidHaskell

tutorial on #liquidhaskell abstract refinements that I wrote a couple years ago and never published before now: https://curious.software/static/absref-draft.html

more than ten years of #haskell and i still have to do this experiment to make sure i'm not wrong
```
ghci> foldr (\el ac -> '(':el:ac++")") "" "abced"
"(a(b(c(e(d)))))"
```
the only time i ever internalized this was when i was writing constructive proofs with #liquidhaskell over folds

I'm going to use #nixpkgs for now and ignore #liquidhaskell at the moment, sadly.

Spending more time on #nixpkgs than coding in #haskell again. Feel motivated to get #liquidhaskell working.

It's sad that #liquidhaskell is broken (liquidpoint marked as broken?) in #nixpkgs right now (right?).

Anyone know what's up with that?

I am yet again starting a project in #haskell and having fun getting lost in something fun, but basically causing me to be side-tracked.

I'm working on a simple pixel art editor, but I am excited by #LiquidHaskell to, I think, use refinement types and prove certain properties about my code.

Learning about #LiquidHaskell!

Have any of you used LiquidHaskell?

#Mechanized #proof of the #commutativity of #zipWith in #LiquidHaskell (continued in replies)

First, we define a type alias with a value argument (it behaves like a macro for refinement types) to describe a proof of the commutativity of some binary function "A":
```
{-@ type Commutative a A = x:a -> y:a -> {A x y == A y x} @-}
```
This says: For some value, A, and for all values x and y, passing x then y to A gives the same result as passing them in the other order.

Towards a translation from Liquid Haskell to Coq. ~ Lykourgos Mastorou, Niki Vazou, Michael Greenberg. https://types2023.webs.upv.es/TYPES2023.pdf#page=125 #ITP #LiquidHaskell #Coq

Assumptions for Liquid Haskell in the large. ~ Facundo Domínguez. https://www.tweag.io/blog/2023-06-22-lh-assumption-imports/ #Haskell #LiquidHaskell #FunctionalProgramming