|
|
|
|
|
|
by nequo
1334 days 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/ |
|
|
- Idris (https://www.idris-lang.org/)
- Agda (https://wiki.portal.chalmers.se/agda/Main/HomePage)
I'm really excited by progress in this space! :)