LinuxConf.Au: Computers, Programs and Logic: What Does Linux Prove?
A Complete Beginner's Introduction to the Mathematics of Computing
Most hackers have heard of Turing Machine, the Halting Problem and the Godel's Incompleteness Theorem. Most hackers firmly believe the the following facts:
- Turing was cool.
- Godel was even cooler.
- Neither Turing nor Godel are relevant to the Linux Kernel.
In the space of 45 minutes, I will endevour to confirm the first two beliefs and refute the third. I will give a complete crash course in the mathematics behind Turing's results and how it applies to the very practical problem of programming in C, without assuming any prior knowledge of formal logic beyond boolean arithmetic.
I will explain the connection between Turing Machines, Lambda Calculus, types, Classical Logic and proofs, and further discuss the place of Godel's Second Incompleteness Theorem in the whole maze.
Without assuming any familiarity with formal reasoning or theorem provers, after the presentation, the audience will have a fundamental understanding of the Curry-Howard Isomorphism that gives the connection between programs, their types, theorems and proofs. They will leave the talk with an understanding of what can and connot be done with C to ensure that their programs are always correct, from the first time they type "make" on the command-line.
At the end of the presentation, the audience will be pointed to open-source tool Twelf that allows practical exploration of the ideas presented in the talk.