I’m not saying I’m right, but I want to understand. What’s the benefits of raw specs with AI, when AI can read the source of truth and explain to you?
In practice, for real systems, this much moves source of truth, as you have pointed out.
However, there is a clear 'compactness' advantage for specs.
Specs can either define the operational (what it does) or the denotational semantics (what it is) for a system, while the code can only be operational. Some things are just easier and better defined in denotational semantics.
It's my understanding that automatic tools were able for a while already to verify whether a given system (code or otherwise) adheres to a given formal specification (at one point after the Pentium bug debacle AMD had its FPU proven, there are variants of the L4 microkernel which were proven, etc.).
The (great) challenge remained to create a formal specification from something humans can write and understand. Isn't that were LLMs come in? And isn't that were the current trust gap remains?
Real software needs mind blowingly complex specifications and while it's now fairly easy to get an AI generated proof that your code follows the spec, there's not much to help you with bugs in the spec.
AI will happily change the spec for you so the code verifies though, but that doesn't solve the trust issue.
Truly a trusting trust scenario.