[meuk]

You're absolutely right, and that's exactly why I am enthusiastic about these fields. I think there is a ton of potential, and that these fields will be booming once the industry discovers this.

Of course, the point is not to prove every program correct. But it should be feasible to prove security-critical parts correct, especially for large companies.

The biggest problem is that formal verification is about as un-sexy as it gets, since it has no applications an sich.