[ayberkt]

Thanks for pointing this out!

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!

[pron]

Right. In computational semantics there are two schools. The "school of Dijkstra" (now championed most vocally by Lamport) -- which has largely taken hold in the field of formal verification -- and the "school of Milner" (Backus?) -- which has largely taken hold in the field of programming language theory. The former reasons in concepts and abstract structures (computations, Kripke structures), and the latter reasons in languages ("calculi").

The interesting philosophical question is this: can programs be said to exist as concepts independent of the language in which they are coded (in which case the language is an artificial, useful construct) or not (in which case the concept is an artificial useful construct)?

Whatever your viewpoint, the "conceptual" state machine math is a lot simpler than the linguistic math offered by PFP.