[adrianratnapala]

I think this is correct -- but.

In Utupia (aka Nowhere) we will have programs that a human being can know is correct. This might involve mathematical proofs, tests and whatever. But how do we know that those things are correct?

In some cases, it would help if we had an English text explaining what the program should doo + computer verification that the program really does that. The English text is only one part of the picture -- but an important part.

This is what acceptance testing tools like Cucumber and Robot try to do; but they avoid actually parsing English. Computers are getting better at parsing human languages, so I expect improvement in this field.