His complaint is that it isn't being done here, so all the prose is jut going to get out of date and incorrect, and meanwhile you have to write everything twice for no benefit.
The problem I see with verifying comments in English (that is, using English as a specification language) is that it's impossible in the general case. So you must, in practice, use a subset of English grammar/nouns which turns into a formal specification language. In turn, this becomes a programming language of sorts, and then we stray away from the goal of "programming languages for humans".
I'd love to be proven wrong, but I think the problem is that this goal itself is mistaken. If we can formally specify something using a language X, this necessarily becomes a language not "for humans" -- i.e. a formal language that doesn't follow the rules of natural language and that we must be trained in. Natural language is notoriously bad at unambiguous specification.
I think there's one kind of "specification language" that works completely unlike programming itself—and that's the interactive form of specification known as requirements-gathering that occurs in the conversation between a contract programmer and their client.
I could see potential in a function-level spec in the form of an append-only transcript, where only one line can be added at a time. So you (with your requirements-specifier hat on) write a line of spec; and then you (as the programmer) write a function that only does what the spec says, in the stupidest way possible; and then you put on the other hat and add another line to the spec to constrain yourself from doing things so stupidly; and on and on. The same sort of granularity as happens when doing TDD by creating unit tests that fail; but these "tests" don't need to execute, human eyes just need to check the function against them.
---
On another tangent: I've never seen anyone just "bite the bullet" on this, acknowledge that what they want is redundant effort, and explicitly design a programming language that forces you to program everything twice in two separate ways. It seems to me that it'd actually be a useful thing to have around, especially if it enforced two very different programming paradigms for the two formalisms—one functional and one procedural, say; or one dataflow-oriented ala APL or J, and the other actor-modelled ala Erlang.
Seems like something NASA would want to use for high-assurance systems, come to think of it. They get part-way there by making several teams write several isolated implementations of their high-assurance code—but it will likely end up having the same flaws in the same places, given that there's nothing forcing them to use separate abstractions.
And then you'd need to describe the specification language and how would that be verified?
I suppose that English is imperfect and could use improvements. Ideally those two would converge. That would solve problems about the interpretation of laws, as well. How would that convergence work? To answer that you'd have to know how language is acquired in the first place. I suppose some form of self-reference in the language that mirrors some of Chomskie's stipulated universal grammar, if it exists.
His complaint is that it isn't being done here, so all the prose is jut going to get out of date and incorrect, and meanwhile you have to write everything twice for no benefit.