BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Microsoft Research Cambridge\, public talks
SUMMARY:Computer science as applied philosophy - Tony Hoar
e\, MSR Cambridge
DTSTART;TZID=Europe/London:20110629T140000
DTEND;TZID=Europe/London:20110629T150000
UID:TALK31932AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/31932
DESCRIPTION:Physics\, Biology\, Medicine\, Mathematics\, and G
eometry all had their origin in Ancient Greek Phil
osophy\; I hope to show that Computing\, considere
d as a branch of Science\, has the same origins in
ancient Greece\; and its practical application to
software engineering sheds light on several histo
ric issues in philosophy.\n\nMy first example is o
f course Aristotle (384-322 bc). His syllogistic l
ogic explained the difference between valid and in
valid reasoning\, not only in Mathematics and the
Natural Sciences\, but also in politics\, law\, an
d philosophy itself. The secret of validity lies s
olely 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 tha
t enables the computer to check very long proofs\,
and actually to discover proofs of conjectures. F
urthermore\, programming languages are defined tod
ay in terms of their syntax\, which permits compil
ers to inhibit execution of meaningless programs.
The meaning of a valid program execution is define
d inductively\, in the same way as a valid logical
proof.\n\nMy next example is Euclid (round 300 bc
). He is the designer of the world’s first program
ming language\, used to specify constructions in g
eometry. His ideas still lie at the basis of all m
odern graphical programming languages\, drawing pi
ctures 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 on
ly language\, in which all the programs come with
a rigorous specification of their purpose\, and a
proof of their correctness. Today\, such proofs ar
e beginning to protect computer programs\, measuri
ng billions of lines of code\, from the risks pose
d viruses\, worms\, and other malware attacks.\n\n
My next example is William of Ockham (1287-1347).
In Medieval times\, the most important application
of logic was to paradoxes of Theology. For exampl
e\, 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 probl
em was solved by Temporal logic\, in a version bas
ed on Branching Time. Today\, computers have been
programmed to use Branching Time in analysis of th
e correctness of communication protocols and compu
ter software designs\, even in the presence of non
-determinism\, which is now a feature of all compu
ter programs and programming languages.\n\nMy fina
l example is Gottfried Leibnitz (1646-1716). He wa
s a co-discoverer with Isaac Newton of the differe
ntial calculus. This works by using symbolic calcu
lations on algebraic formulae. The correctness of
the calculation is defined by the list of algebrai
c equations that are presented by the calculus. Le
ibnitz had a dream that all the truths of philosop
hy\, theology and natural science could be derived
from first principles by just such calculations.
This dream is now being partially realised in mass
ive computer data-bases\, which can find evidence
that supports or refutes any conjecture presented
by scientists or doctors.\n\nIn the last century\,
the link between Computer Science and Philosophic
al Logic became even more intense. George Boole in
vented Boolean algebra\, which lies at the basis o
f all computer hardware\, as well as the Propositi
onal Calculus\, which is the basis of all proofs\,
both in Computer Science and in Mathematics. Gott
lob Frege formalised the predicate calculus in a m
anner that is now recognised as adequate for all o
f mathematical proof. His formalisation of bound v
ariables is now incorporated in the declarations o
f all computer programming languages. Bertrand Rus
sell was most concerned with avoiding the paradoxe
s that he discovered at the very foundations of ma
thematics. He invented a theory of types to solve
the problem. Types are used in most computer langu
ages of the present day to inhibit the execution o
f meaningless programs. The mathematician David Hi
lbert hoped to prove the consistency of mathematic
s by means of a new specialised branch of Mathemat
ics (Metamathematics)\, whose subject matter is ma
thematical formulae\, rather than sets or numbers
or geometric figures. This gave Alan Turing the id
ea of a computer that is capable of operating on p
rograms held in its own store: although his motive
was to prove that Hilbert’s hope for mathematics
was impossible.\n\nI will not have time to deal wi
th the twentieth Century\, so I refer you to the e
xcellent book ‘Engines of Logic’ by Martin Davis.\
n
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7
J J Thomson Avenue (Off Madingley Road)\, Cambrid
ge
CONTACT:Microsoft Research Cambridge Talks Admins
END:VEVENT
END:VCALENDAR