> > And in practice, the only form of verified formal proof of properties of program fragments that sees use in "normal" industrial code (i.e. ordinary webapps and the like, not high-assurance environments) is Haskell-like typesystems

> This is 100% false. Haskell's type system (without clever tricks such as singleton types) is so weak that the properties it "verifies" fall far, far below what is normally regarded as "formal verification".

Be careful to pay attention to what lmm actually claimed. The claim was about "proof of properties of program fragments ... in "normal" industrial code ... ordinary webapps".