3 ms·
> Having strong typing doesn't magically do formal validation on your logic There are plugins for Haskell and dependently typed languages that go much further
by tluyben2 4y ago
> Having strong typing doesn't magically do formal validation on your logic
There are plugins for Haskell and dependently typed languages that go much further in the ‘if it compiles, it is formally validated’, but that’s a lot more work; there is a trade-off for now or you will be stuck. Your ‘run of the mill’ tests also don’t formally validate your logic (not even close usually). Our types, even if static, are usually too loose and our type systems not powerful enough; writing tests helps to close the gap between practical and theoretical but a lot more can be done semi-automatically (and will be I hope).
- 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! :)