Writing a small computer program is easy. Designing and producing a complete software program that is reliable, durable and resistant to attack remains extraordinarily difficult. It is the aim of Software Science to design and develop the principles, mathematical formalisms, empirical techniques and computational tools needed to design, program and verify reliable, secure software.

The lectures at Software Science aim to explore these issues and present contemporary research in the field. The lecture focuses on approaches known as " formal ", as opposed to the empiricism often used in software engineering. These approaches are based on known or emerging mathematically rigorous foundations : formal semantics, program logic, deductive systems, program equivalence, process calculus... Historically, these concepts emerged from very down-to-earth programming considerations before being adorned with mathematical rigor. The lecture traces this progression of ideas from the programmer's intuition to the mechanization of these formal approaches.

The first years of this lecture could have been entitled " Programming, demonstrating ", as they explored several modes of interaction between software programming and the demonstration of mathematical statements : programming then demonstrating, as in program logics for deductive verification ; programming to demonstrate, as in constructive logics and the demonstration assistant Coq ; finally, programming equals demonstrating, as in the fruitful Curry-Howard correspondence, the subject of the first year of the lecture.

Research at the Software Science chair is carried out within the framework of the Cambium project-team, a joint venture with Inria. The team's work aims to improve the reliability, safety and security of software by advancing programming languages and formal program verification methods. The main research themes are type systems and type inference algorithms, deductive program verification, shared-memory parallelism and weakly consistent memory models. The team designs and develops two major research software packages that integrate and translate many of its results into practice : OCaml, a statically typed functional programming language and its implementation, and CompCert, a formally verified compiler for mission-critical embedded software.