This is what attracted me to FP to begin with, the "if it compiles it works" meme. Program verification and functional programming are separate things. Ada pre

This is what attracted me to FP to begin with, the "if it compiles it works" meme. Program verification and functional programming are separate things. Ada predates Haskell by at least a decade, and it's not functional at all. Rust is kind of a revival of that in proving memory safety via borrowing; not functional either. But the set of programs which can be formally proven is smaller than the set of all programs, so I'd rather not miss out by only making formally proven software. (The entire field of deep learning is a good example of useful code which can't be formally proven.)