> that there are fully verifiable imperative languages out there (with their own serious problem -- correctness is never free), that have actually been used by

> that there are fully verifiable imperative languages out there (with their own serious problem -- correctness is never free), that have actually been used by the industry to write some very important, safety-critical software, and have been actually put to the test much more than Haskell. Ada is absolutely painful to work with as a developer (I used to work in Aerospace). But if you could get your code to compile, it stood a very good chance of just working.