[auggierose]

I wouldn’t split it like that. Formal verification is useful in the case that the spec is simpler than the implementation. That’s it.

Coming up with simple specs is not necessarily easy. You could say that is kind of what math is about. That’s how we actually make progress: find those cases where simple specs are possible and build upon them. That’s the kind of library made for eternity.

[oulipo2]

It could still be useful if the spec is roughly as hard as a simple implementation, in case you have automated methods to find more efficient implementations, guided by the constraints of the spec

[auggierose]

Which is still a case of the spec being simpler than the implementation (you are after) ;-)

Very often, the spec is indeed just a very simple implementation. Often you can make the spec especially simple if there are no constraints on the resources it can use, at times even infinite ones.

[Animats]

Right. Databases can be modeled as linear search over huge arrays, for example.