Computer science as applied philosophy

Add to your list(s) Download to your calendar using vCal

• Tony Hoare, MSR Cambridge
• Wednesday 29 June 2011, 14:00-15:00
• Large lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

Physics, Biology, Medicine, Mathematics, and Geometry all had their origin in Ancient Greek Philosophy; I hope to show that Computing, considered as a branch of Science, has the same origins in ancient Greece; and its practical application to software engineering sheds light on several historic issues in philosophy.

My first example is of course Aristotle (384-322 bc). His syllogistic logic explained the difference between valid and invalid reasoning, not only in Mathematics and the Natural Sciences, but also in politics, law, and philosophy itself. The secret of validity lies solely in the syntactic form of the argument, and is completely independent of its subject matter in the real world. Today, it is a formal syntax that enables the computer to check very long proofs, and actually to discover proofs of conjectures. Furthermore, programming languages are defined today in terms of their syntax, which permits compilers to inhibit execution of meaningless programs. The meaning of a valid program execution is defined inductively, in the same way as a valid logical proof.

My next example is Euclid (round 300 bc). He is the designer of the world’s first programming language, used to specify constructions in geometry. His ideas still lie at the basis of all modern graphical programming languages, drawing pictures on all the screens of all the computers and cinemas and telephones in the world. His language was certainly the 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 programs, measuring billions of lines of code, from the risks posed viruses, worms, and other malware attacks.

My 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 perfect knowledge of the Deity of what is going to happen in the future with the existence of man’s free will. This problem was solved by Temporal logic, in a version based on Branching Time. Today, computers have been programmed to use Branching Time in analysis of the correctness of communication protocols and computer software designs, even in the presence of non-determinism, which is now a feature of all computer programs and programming languages.

My final example is Gottfried Leibnitz (1646-1716). He was a co-discoverer with Isaac Newton of the differential calculus. This works by using symbolic calculations on algebraic formulae. The correctness of the calculation is defined by the list of algebraic equations that are presented by the calculus. Leibnitz had a dream that all the truths of philosophy, theology and natural science could be derived from first principles by just such calculations. This dream is now being partially realised in massive computer data-bases, which can find evidence that supports or refutes any conjecture presented by scientists or doctors.

In the last century, the link between Computer Science and Philosophical Logic became even more intense. George Boole invented Boolean algebra, which lies at the basis of all computer hardware, as well as the Propositional Calculus, which is the basis of all proofs, both in Computer Science and in Mathematics. Gottlob Frege formalised the predicate calculus in a manner that is now recognised as adequate for all of mathematical proof. His formalisation of bound variables is now incorporated in the declarations of all computer programming languages. Bertrand Russell was most concerned with avoiding the paradoxes that he discovered at the very foundations of mathematics. He invented a theory of types to solve the problem. Types are used in most computer languages of the present day to inhibit the execution of meaningless programs. The mathematician David Hilbert hoped to prove the consistency 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 store: although his motive was to prove that Hilbert’s hope for mathematics was impossible.

I will not have time to deal with the twentieth Century, so I refer you to the excellent book ‘Engines of Logic’ by Martin Davis.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Large lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.