> you might have two algorithms for computing the same thing, one simple and obviously right, and one complex and optimized.

Right. Those are the kinds of systems that are easy to specify concisely. Databases, for example, can be specified as giant arrays with linear search.