> I have trouble understanding the usefulness of this. Haskell is barely used in the first place, and even less for highly safety critical software. Every new

> I have trouble understanding the usefulness of this. Haskell is barely used in the first place, and even less for highly safety critical software. Every new approach is initially barely used in the wild, and the initial method of such a new approach is usually quite different in details from how things end up eventually. In this case the value lies in working out how proving software could look like, and proving program after writing it is a different direction than writing it to a proof. We can't tell which of these methods is more useful or convenient before somebody checks them out.