Comment by kmacdough

Computers can and should help along the way, but Dijkstra's argument is that a) much of the challenge of human ideas is discovered in the act of converting from natural to formal language and b) that this act, in and of itself, is what trains our formal logical selves.

So he's contesting not only the idea that programs should be specified in natural language, but also the idea that removing our need to understand the formal language would increase our ability to build complex systems.

It's worth noting that much of the "translation" is not translation, but fixing the logical ambiguities, inconsistencies and improper assumptions. Much of it can happen in natural language, if we take Dijkstra seriously, precisely because programmers at the table who have spent their lives formalizing.

There are other professions which require significant formal thinking, such as math. But also, the conversion of old proofs into computer proofs has lead us to discover holes and gaps in many well accepted proofs. Not that much has been overturned, but we still do t have a complete proof for Fermats last theorem [1].

[1] https://xenaproject.wordpress.com/2024/12/11/fermats-last-th...