|
|
|
|
|
|
by munro
4068 days ago
|
|
|
> ML-family and Haskell are popular where provable correctness is wanted. Haskell doesn't have a theorem prover, you may want to check out Idris [1]. Haskell gives you more safety that you aren't going to get run time errors than say Java, but not completely. You'll still need automated testing for correctness, that you're not getting garbage in, garbage out. [1] http://dafoster.net/articles/2015/02/27/proof-terms-in-idris... |
|
|