Here’s Edsger Dijkstra discussing the birth of the use of axiomatics in computer science – the start of “formal methods” research. What’s striking is the assumed choice between “axiomatic” and “mechanistic” as if there was no other way. In a
Recursion and state
Despite some deep results, algebraic automata theory has fallen out of favor in theoretical computer science. Reasons include the disciplines failings such as a love of over-generality, weak mathematical background of people working on “formal methods”, and gap between theoreticians
Are threads evil? (updated)
This paper by Prof. Edward Lee explains something of why “threads” are such a painful abstraction. As Prof. Lee notes, threads intrinsically create unspecified program operation (which he calls non-determinism) and resource conflicts which we then attempt to “prune” via
Updated Dijkstra vs Perlis (really, DeMillo)
See below.
Dijkstra versus Perlis (updated)
Dijkstra wrote: He [Perlis] published a very obnoxious paper arguing against a mathematical approach to programming cite The paper by De Millo, Lipton and Perlis starts as follows: Many people have argued that computer programming should strive to become more like mathematics.
Meaning of concurrent programs and IP
Most of the new draft of the Concurrent Programs paper has to do with trying to specify problems and solutions in synchronization via an atomic “compare and swap” operation. Even these operations are surprisingly complicated once put under the microscope
Updated: meaning of concurrent programs
Updated rough draft available with thrilling descriptions of atomic compare and swap and some comments on “formal methods”. Bonus photo
New paper “H2” on operating system semantics
Please see a new version here. I am continuing to try to develop a practical engineering mathematics for operating system and other complex system code.