Re:Interfaces All the Way Down
by formulathree on Sunday July 23, 2023 @03:44PM
(#36839001)
I'm more thinking in terms of logical primitives for the design of modules and components that can be composed, decomposed and recombined. I'm thinking less about proof based correctness.
Look up Coq, Agda, Lean, and Idris. I would start with Coq, it's the most used. Idris is more like Haskell and programmer-oriented.
Edit: Nevermind, apparently they were just talking about Haskell...