> 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).
> 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.
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).