BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Computer science as applied philosophy - Tony Hoare\, MSR Cambridg
 e
DTSTART:20110629T130000Z
DTEND:20110629T140000Z
UID:TALK31932@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Physics\, Biology\, Medicine\, Mathematics\, and Geometry all 
 had their origin in Ancient Greek Philosophy\; I hope to show that Computi
 ng\, considered as a branch of Science\, has the same origins in ancient G
 reece\; and its practical application to software engineering sheds light 
 on several historic issues in philosophy.\n\nMy first example is of course
  Aristotle (384-322 bc). His syllogistic logic explained the difference be
 tween valid and invalid reasoning\, not only in Mathematics and the Natura
 l Sciences\, but also in politics\, law\, and philosophy itself. The secre
 t of validity lies solely in the syntactic form of the argument\, and is c
 ompletely independent of its subject matter in the real world. Today\, it 
 is a formal syntax that enables the computer to check very long proofs\, a
 nd actually to discover proofs of conjectures. Furthermore\, programming l
 anguages are defined today in terms of their syntax\, which permits compil
 ers to inhibit execution of meaningless programs. The meaning of a valid p
 rogram execution is defined inductively\, in the same way as a valid logic
 al proof.\n\nMy next example is Euclid (round 300 bc). He is the designer 
 of the world’s first programming language\, used to specify construction
 s in geometry. His ideas still lie at the basis of all modern graphical pr
 ogramming languages\, drawing pictures on all the screens of all the compu
 ters and cinemas and telephones in the world. His language was certainly t
 he first\, and still almost the only language\, in which all the programs 
 come with a rigorous specification of their purpose\, and a proof of their
  correctness. Today\, such proofs are beginning to protect computer progra
 ms\, measuring billions of lines of code\, from the risks posed viruses\, 
 worms\, and other malware attacks.\n\nMy next example is William of Ockham
  (1287-1347). In Medieval times\, the most important application of logic 
 was to paradoxes of Theology. For example\, how do you reconcile the perfe
 ct knowledge of the Deity of what is going to happen in the future with th
 e existence of man’s free will. This problem was solved by Temporal logi
 c\, in a version based on Branching Time. Today\, computers have been prog
 rammed to use Branching Time in analysis of the correctness of communicati
 on protocols and computer software designs\, even in the presence of non-d
 eterminism\, which is now a feature of all computer programs and programmi
 ng languages.\n\nMy final example is Gottfried Leibnitz (1646-1716). He wa
 s a co-discoverer with Isaac Newton of the differential calculus. This wor
 ks by using symbolic calculations on algebraic formulae. The correctness o
 f the calculation is defined by the list of algebraic equations that are p
 resented by the calculus. Leibnitz had a dream that all the truths of phil
 osophy\, theology and natural science could be derived from first principl
 es by just such calculations. This dream is now being partially realised i
 n massive computer data-bases\, which can find evidence that supports or r
 efutes any conjecture presented by scientists or doctors.\n\nIn the last c
 entury\, the link between Computer Science and Philosophical Logic became 
 even more intense. George Boole invented Boolean algebra\, which lies at t
 he basis of all computer hardware\, as well as the Propositional Calculus\
 , which is the basis of all proofs\, both in Computer Science and in Mathe
 matics. Gottlob Frege formalised the predicate calculus in a manner that i
 s now recognised as adequate for all of mathematical proof. His formalisat
 ion of bound variables is now incorporated in the declarations of all comp
 uter programming languages. Bertrand Russell was most concerned with avoid
 ing the paradoxes that he discovered at the very foundations of mathematic
 s. He invented a theory of types to solve the problem. Types are used in m
 ost computer languages of the present day to inhibit the execution of mean
 ingless programs. The mathematician David Hilbert hoped to prove the consi
 stency of mathematics by means of a new specialised branch of Mathematics 
 (Metamathematics)\, whose subject matter is mathematical formulae\, rather
  than sets or numbers or geometric figures. This gave Alan Turing the idea
  of a computer that is capable of operating on programs held in its own st
 ore: although his motive was to prove that Hilbert’s hope for mathematic
 s was impossible.\n\nI will not have time to deal with the twentieth Centu
 ry\, so I refer you to the excellent book ‘Engines of Logic’ by Martin
  Davis.\n
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR