[adrianN]

No progress in language theory can fix the fundamental problem of software verification: you need a formal specification to have anything to verify. Who wants to write not only a detailed spec for their code, but a spec that has well defined semantics in some kind of logic? Nobody, that's who. There are very few properties that you care about that are both sufficiently easy to encode in a formal specification and not provided automatically by a safe language.

[joe_the_user]

Even more, software development now involves an assumption of the average manager or customer that some extra feature can be added halfway through.

Is the customer going to be happy with "we've billed $X for a formal spec and that means that we can't make the change that you want, that seems simple without $Y dollars for changes to it and the code." Notice that software methodologies have gone the opposite direction here, with Extreme Programming basically aiming to make all of the programmer's activities revolve around exactly what and only what the customer has actually requested.

[seventhtiger]

But the features are not arbitrary. The vast majority of features are common among many applications, and a template formal spec can be built to satisfy those features. Once formal spec of the building blocks is created, there will only be the small portion of unique code that needs a unique formal spec.

[whatshisface]

In the logical extreme that can't be the case, because a fully debugged program plus a machine to run it on actually satisfy the definition of a formal specification. Deciding what you want your program to do is the eternal burden of programming, but maybe there's a way to make formal specification at least as easy as regular programming.

[adrianN]

But then you already have a perfect implementation that you somehow made without the use of formal verification. But you want to introduce formal verification because translating real-world requirements into a formal language is hard enough that you can't be sure of correctness...

[xamuel]

One example of something you'd always like to verify is, "this code does not have undefined behavior". This could be the key to obtaining C speed without C's lack of safety. In fact, in some possibly-formalizable sense, it's probably the ONLY way to do that.