> must be able to express the same rigor in less words than existing source code

Yes but also no. Writing source means rigorously specifying the implementation itself in deep detail. Most of the time, the implementation does not need to be specified with this sort of rigor. Instead the observable behavior needs to be specified rigorously.

That doesn't sound right. For example, there's plenty of software with the correct observable behavior which leaks credentials. So what needs to be captured goes beyond observable behavior.