(image produced by Stable Diffusion)
The expressive type system of OCaml brings strong static safety guarantees by ensuring data is used in a consistent way by a program. The Salto project aims at providing OCaml programs with additional guarantees, by answering questions such as:
Those questions are beyond the scope of the OCaml type system, but are within reach of abstract interpretation-based static analyses.
The goal of the Salto project is to define sound static analyses that help answer the above questions as automatically as possible. The analysis will help a programmer have better confidence in her programs, by bringing increased safety and security guarantees.
The Salto project is a partnership between Nomadic Labs and Inria, and is funded by the Tezos Foundation.