> two programs can both satisfy the same spec and have completely different

The spec should express all relevant constraints. If your spec admits two things and only one is admissible in your mind, your spec is incomplete.

> has a massive envelope

The size of the envelope is less relevant than the expressivity of the language used to express subsets of that envelope. But almost always there is some logic which is more succinct for expressing the spec than the programming language used to express the implementation.

> your security posture is now a function of how exhaustive your spec is

The alternative is that your security posture is a function of unstated intentions living in somebody’s brain. This alternative seems strictly worse.

> You'd need to enumerate what NOT to do

This is equivalent to declaring what you must do and usually there is a succinct way to do this that does not involve listing every negative example