3 ms·
> There are plugins for Haskell and dependently typed languages that go much further in the ‘if it compiles, it is formally validated’ Yes, Lean 4[1] is shapin
by nequo 4y ago
> There are plugins for Haskell and dependently typed languages that go much further in the ‘if it compiles, it is formally validated’
Yes, Lean 4[1] is shaping up to be a Haskell-inspired dependently typed language with monadic IO etc. that can also prove theorems for you. Still a work in progress but looks very exciting.
[1] https://leanprover.github.io/lean4/doc/ https://leanprover.github.io/lean4/doc/
- epgui 4y agoSee also: - Idris (https://www.idris-lang.org/ https://www.idris-lang.org/) - Agda (https://wiki.portal.chalmers.se/agda/Main/HomePage https://wiki.portal.chalmers.se/agda/Main/HomePage) I'm really excited by progress in this space! :)