Let's define success as new + useful. You can build something new then make it useful, or you can start with useful and add something new.
I suggest that the second approach is better, because we already have a good sense of how to measure useful, so you will always know where you are. Keep your eyes on the prize, as they say.
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.
I think you're missing that this was was research project, and they were trying to answer the fundamental question, can we build a verifiable systems language?
I suggest that the second approach is better, because we already have a good sense of how to measure useful, so you will always know where you are. Keep your eyes on the prize, as they say.