Thursday, 19 April 2007, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: We are today at the dawn of a new way of doing mathematics and computer science. Computers are increasingly used to develop and verify mathematical theories. On the other hand, computer programming is becoming richer, with more expressive data types and programming techniques. Eventually the two fields will converge and become a single entity: Computer Mathematics.
I will discuss the relations between mathematics, logic, and computer science. I hope to convince you that dramatic advances in these connections are on the horizon that will radically change these fields.
From ancient times until 1800s, mathematics was mostly concerned with computing solutions to problems. In the second half of the nineteenth century, abstract notions were developed and the doctrine of mathematics as the study of pure absolute truth took hold.
As mathematics grew more and more incorporeal and nonconstructive, two other important developments took place: a deep crisis in the logical foundations of mathematics and, later, the development of the cornerstones of computer science.
A connection between logic and computer science, called realizability, was developed. It represented proofs in predicate logic as natural numbers and proof steps as arithmetical operations. A refinement of this conception led to represent proofs as programs in a typed language. This is called the Curry-Howard isomorphism. Per Martin-Löf developed a rich type theory that can be seen at the same time as a programming language, a logical system, and a mathematical universe.
Subsequently the theory grew by additions of new constructs and operations. However, many problems still need to be solved, before type theory becomes a complete environment to develop mathematics on a computer. Here are the problems that I consider more pressing: