3 ms·
Very informative slides. I do not have real-world experience with Haskell, aside from little toy projects, but I have a lot of experience with other functional
by nextos 6y ago
Very informative slides.
I do not have real-world experience with Haskell, aside from little toy projects, but I have a lot of experience with other functional languages in the ML family and Scheme.
Idris 2 looks appealing, but they should have also mentioned other approaches like Fstar, Lean and Z3. I quite like Fstar since they are delivering a big verified code base, as implied by the name of the effort: Project Everest [1].
While theorem proving is the most general approach to verification, manual proofs are tedious and full automation might never be completely possible in the short term.
I would love to see someone pushing for a different approach. A toolkit where you can create DSLs with limited expressiveness, which in turn make it easy to build and verify things. The equivalent to Alan Kay's Viewpoints Research Institute efforts to build a minimal computation system, but with some verification guarantees.
[1] https://project-everest.github.io/ https://project-everest.github.io/
- philzook 6y agoThose are interesting approaches. I'm pretty pumped about Lean. It may just not have fit into his narrative and he can't talk about everything. Fstar and Lean are more children of Coq and ML (at least syntactically) to my understanding than they are children of Haskell. They're cousins. Although everyone influences everyone of course.
- logicchains 6y ago>A toolkit where you can create DSLs with limited expressiveness, which in turn make it easy to build and verify things. This is a common approach in the Coq ecosystem, writing DSls for building things, and custom automation for them. See for instance papers by Adam Chlipala.
- nextos 6y agoI know. His FRAP & CPDT books are great reads.