> Writing MISRA C and using verification tools like Astree, or SPARK + verification tools are not as elegant, but their weakest point is stronger than Haskell's

> Writing MISRA C and using verification tools like Astree, or SPARK + verification tools are not as elegant, but their weakest point is stronger than Haskell's. That's why we need more Haskell-hosted system programming DSLs - with fancy sound types, proofs, extraction and stuff.