The claim: we have demonstrated the comprehensive formal verification of the seL4 microkernel, with a complete proof chain from precise, formal statements of high-level security and safety properties to the binary executable code. GD The L4 base is useful –
State machines and circuits
The cross coupled latch is one of the greatest inventions of the 20th century State machine models of timing and circuit design
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.