3 ms·

Agreed- that's why I said in the beginning I'm only talking about design verification. Verifying code is a long way off from going mainstream. I talk about the

• zozbot234 7y ago
  I assume you mean "full" code verification in some sense. Partial verification, especially of properties that are "local" and where verification can be done in a way that's "based" on the language syntax itself, is relatively common. This kind of verification is often called "type checking" and is often not even thought of as a means of code verification. One can of course object that requiring the use of a language where verification is "baked in" like this might be undesirable; but either way, it seems clear even to formal-methods proponents that well-chosen language semantics are going to be very important if code verification is to be feasible. So it's six of one, half a dozen of the other.