[ncmncm]

In practice, expressible specs are always, always, always incomplete. Some requirements just don't fit into any usable formalism. Some that do fit unavoidably overspecify behavior, so that, e.g. more efficient, acceptable behavior would be disqualified.

There are reasons why we don't just write formal specs and generate a system from them. It is not just stubbornness.

What is astonishing is that certain, isolated systems have been generated from formally complete specs. They need to recognized as miraculous, unique and unrepeatable.