Makes me think of this commitstrip comic: https://i.xkqr.org/itscalledcode.jpg (mirrored from the original due to TLS issues with the original domain.)

A guy with a mug comes up to a person standing with their laptop on a small table. The mug guy says, "Some day we won't even need coders any more. We'll be able to just write the specification and the program will write itself."

Guy with laptop looks up. "Oh, wow, you're right! We'll be able to write a comprehensive and precise spec and bam, we won't need programmers any more!"

Guy with mug takes a sip. "Exactly!"

Guy with laptop says, "And do you know the industry term for a project specification that is comprehensive and precise enough to generate a program?"

"Uh... no..."

"Code. It's called code."

Goodhart's Law of Specification: When a spec reaches a state where it's comprehensive and precise to generate code, it has fallen out of alignment with the original intent.

Of course there are some systems where correctness is vital, and for those I'd like a precise spec and proof of correctness. But I think there's a huge bulk of code where formal specification impedes what should be a process of learning and adapting.

My dream antiprogram is a specification compiler that interprets any natural language and compiles it to a strict specification. But on any possible ambiguity it gives an error.

    ?