alt Hacker NewsI somewhat disagree with this. In real life, say in some company, the inception of an idea for a new feature is made in the head of some business person. This person will not speak any formal language. So however you turn it, some translation from natural language to machine language will have to be done to implement the feature.
Typically the first step, translation from natural to formal language, will be done by business analysts and programmers. But why not try to let computers help along the way?
Replies
The first step isn't from natural language to formal language. It's from the idea in your head into natural language. Getting that step right in a way that a computer could hope to turn into a useful thing is hard.
Say, doesn't each business - each activity - have its own formal language?
Not as formalized as programming languages, but it's there.
Try to define any process, you end up with something trending towards formalized even if you don't realize it.
I like your take.
The only issue I have with trusting a computer to do so much is that it doesn't necessarily have the long term vision or intuition some humans might have for the direction of the software product. There's so much nuance to the connection between a business need and getting it into software, or maybe I am overthinking it :D
I don't think youre fully comprehending Dijkstra's argument. He's not saying to not use tool to help with translation, he is saying that not thinking in terms of formal symbols HURTS THINKING. Your ideas are worse if you don't think in formal systems. If you don't treat your thoughts as formal things.
In your example, he has no opinion on how to translate the idea of a "business person" because in his view the ideas of the "business person" are already shallow and bad because they don't follow a formalism. They are not worth translating.
Because then you don't know what the computer's doing. The whole point of this article was that there is value in the process of writing your ideas out formally. If you "let computers help you along the way", you'll run straight into the issue of needing an increasingly formal natural language to get sufficiently good results from the machine.
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...