Dijkstra, in his "on the cruelty of really teaching computing science" makes a very similar point that people should learn how to reason about programs before learning to program.
This is why dependent types are a great framework to program in. If a program is worth writing, it should at least contain everything the programmer thinks about the program, including the reasoning of why it is the program he wants to write!
Dijkstra, in his "on the cruelty of really teaching computing science" makes a very similar point that people should learn how to reason about programs before learning to program.
This is why dependent types are a great framework to program in. If a program is worth writing, it should at least contain everything the programmer thinks about the program, including the reasoning of why it is the program he wants to write!