If the goal was to make a C-like language that's verifiable, though, and you end up with a C-like language that isn't verifiable, in what sense is that useful? The whole usefulness of the project, at least as it was conceived, hinged on it adding some notion of verifiability to C. Otherwise it's just a C clone with smaller installed base, worse tool support, etc.
There are degrees of verifiability. A C-like language with imperfect but stronger verifiability (for example, with a strong, formalized type system) is still more verifiable (admits the proof of more theorems via static analysis) than C.
The whole usefulness of the project, at least as it was conceived, hinged on it adding some notion of verifiability to C.
That is exactly what I am saying. It sounds like they trimmed away too much of C in the process and didn't check to make sure those parts could be added back. I haven't really followed the whole saga though.
