Software Science

Writing a small computer program is easy. Designing and building a complete software system that is reliable, sustainable, and resistant to attacks remains extraordinarily difficult. The goal of Software Science is to design and develop the principles, mathematical formalisms, empirical techniques, and computational tools necessary to design, program, and verify reliable and secure software.

The curriculum of the Software Science Chair aims to explore these issues and present contemporary research in this field. The course emphasizes so-called “formal” approaches, as opposed to the empiricism often prevalent in software engineering. These approaches are based on mathematically rigorous foundations, whether established or emerging: formal semantics, program logic, deductive systems, program equivalences, process calculi… Historically, these concepts emerged from very down-to-earth programming considerations before being imbued with mathematical rigor. The course strives to trace this evolution of ideas, starting from the programmer’s intuition and extending to the mechanization of these formal approaches.

The first years of this course could have been titled “Programming, Proving,” as they explored several modes of interaction between software programming and the proof of mathematical statements: programming and then proving, as in program logics for deductive verification; programming to prove, as in constructive logics and the Coq proof assistant; finally, programming equals proving, as in the fruitful Curry-Howard correspondence, the subject of the first year of the course. Subsequent years explore other facets of Software Science, notably the comparative study of programming languages and software security, through “language-based” or cryptographic approaches.

Research at the Software Science Chair is conducted within the Cambium project team, a joint initiative with Inria. The team’s work aims to improve the reliability, safety, and security of software by advancing programming languages and methods for the formal verification of programs. The main research themes are deductive program verification, type systems and type inference algorithms, and shared-memory parallelism. The team designs and develops two major research software projects that integrate and put many of its results into practice: OCaml , a statically typed functional programming language and its implementation, and CompCert , a formally verified compiler for critical embedded software. In 2021, CompCert received the ACM Software System Award , the highest honor for research-based software.