Problem is, usually describing the problem you want to solve *correctly* using formal tool is a task as hard (and often, equivalent to) the implementation. That said, having a formal description is useful

▲

Animats 7 hours ago | parent [-]

For some problems, yes. Formal specification is particularly useful in two cases. 1) The problem is simple but an efficient implementation is hard or bug-prone. Examples are garbage collection, file systems, sorts, databases, and tree updating. 2) The inverse of the problem is simpler than the forward operation. Examples include matrix inversion and parsing.

▲

auggierose 7 hours ago | parent [-]

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 4 hours ago | parent [-]

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 3 hours ago \| parent [-]
		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.