Dale Miller: “Making proof universal”

One thing of which Dale Miller is convinced is that the securing of ERC funding is going to help both him and Parsifal, his project-team, make significant progress along the long path towards proof. And this progress is set to benefit everyone! This proof is somewhat akin to the Holy Grail for computer-science and mathematics researchers. How can it be proved that a software program or an electronic circuit does exactly what is expected of it, and that it does so under the conditions and in compliance with the specifications that presided over its creation? To prove the validity of a program featuring several million code lines, it is sometimes necessary to design a new program, itself composed of several hundred thousand code lines…

It is a subject that is far from trivial. Digital systems are multiplying in number, and not just in the fields of leisure activities or entertainment, where the user can restart the system themselves in the event of an error, or manage without a particular function if it is affected by a bug. Today, codes and programs guide, control and automate many tasks that have an impact on our daily lives, and that cannot tolerate malfunctioning of any kind. The launch of a rocket  that is to release a communications satellite supposed to work autonomously for fifteen or so years must be made 100% reliable. Likewise, in the monitoring of the temperature of an incubator  or the heart rate of a patient who has just undergone heart surgery, there is no room for faults. Not to mention airliners, bank transaction systems, telecommunications, etc. In addition, there is the question of security: how can we protect all of these digital objects from viruses and malicious attacks?

Dale Miller has been working on these subjects for quite some time. After achieving a Ph.D. in mathematics at the university of Carnegie Mellon, he became a computer-science professor and researcher. He first worked in the United States, and then in Europe, where his subject, computational logic, has met with great interest within research circles. He was particularly attracted by the cities of Edinburgh, Glasgow, Genoa, Pisa and Siena, but it is in France that he has finally settled. An American married to an Italian, he moved to the Paris region in 2002 when he took on the roles of senior research scientist at the Inria Saclay centre and professor at the Ecole Polytechnique. His level of French does not quite measure up to his commitment to French research, “I’d have to leave the lab if I wanted to speak French properly”, he says. It is true that he is surrounded by a very cosmopolitan team on a daily basis: a German, an American, an Indonesian, Dutch, Italians... and French nationals, and that in research the working language remains English!

The idea is to create a market place where it will be possible to exchange and share the proof systems developed in different locations.

He mentions the Tower of Babel, not in reference to the multilingualism of his environment, but rather to describe the situation as regards proof. “No standard exists within this field. Every time proof is needed that a system works, a budget and a student are required in order to develop a verifier of the system's property proofs. Moreover, this verifier is designed on an ad hoc basis and functions for a single system only. At times it does not even work for the subsequent version of the same system!” The most explicit counter example is that of text files: “ever since the invention of html language, it has been possible for files to be read by any browser. This is what we wish to achieve within the field of proof.”

His idea: to perform “computer-science chemistry”, that is, use the atoms of existing inferences to develop molecules of inferences. In other words, to offer certified proof-system modules in order to be able to compose an arbitrary system... “The idea is to create a market place where it will be possible to exchange and share the proof systems developed in different locations.” In order to achieve this, Dale Miller envisages issuing “proof certificates”; this is the purpose of the ProofCert project that won him the ERC grant. “The subject is actually very abstract, but it has a definite impact on the real world and on our lives...”
he concludes.