FRESCO is a research project aimed at building a new programming environment for fast and verified symbolic computation.
This project will be generously funded for five years by an ERC Consolidator grant. The core team is located in University of Nantes, in the Gallinette Inria team-project, with some members hosted in Paris Saclay University, in the Toccata Inria team-project.
Contents: News ⋅ Goals ⋅ Members
Computers have changed the face of research in mathematics. They have dramatically augmented experiment and guesswork. Groundbreaking conjectures were only made accessible by resorting to superhuman computational power, e.g., Mandelbrot's fertile observations in fractal geometry, or Birch and Swinnerton-Dyer's conjecture, for which the Clay Institute advertises a $1 million bounty. In fact, they have also revolutionized the essence of what a proof is. Starting with the Four Color theorem, about the coloration of planar maps, the list of computer-assisted proofs of major mathematical results has grown steadily, covering a broad range of mathematical fields: combinatorics, optimization, number theory, dynamical systems, etc.
Computer proofs are essentially produced by symbolic computations, on exact data such as (unbounded) integers, rational numbers, polynomials, matrices. Computer algebra systems are the main vehicle of symbolic methods. Besides the libraries implementing cutting-edge fast algorithms, these complex systems are also powered by a domain specific language, used to formulate queries, and sophisticated graphical interfaces, which allow to produce documents interleaving text and graphics, with calculations. But “are we just getting wrong answers faster?” Stadtherr's unkind question to the community of high-performance computing not only remains valid today, but it extends to the realm of computer algebra. While machine-assisted design and verification have become standard for critical systems or when security and privacy issues are at stake, only makeshift techniques are available for auditing computer-produced mathematics, far behind the current state of the art in program verification.
New theoretical and practical tools are needed to produce, and reason about, computer-aided mathematics, with no compromise on speed nor on reliability. Our grand challenge is thus to deliver fast yet reliable symbolic computations to the users of computer algebra systems. For this purpose, we will design a novel generation of mathematical software, based on the firm grounds of modern programming language theory. In particular, the main vision behind the FRESCO project is a verified compilation scheme from textbook formulas to machine code, with feedback to formal proofs. Using Coq's higher-order, dependently typed, programming language we can express all these steps, specify and verify each transformation phase, and reuse the result in a broader formal proof context.
|
|
|