(image produced by DALL·E)
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.
salto-IL,
the intermediate language that is used by the Salto analyser,
and the transformation from the OCaml Typedtree to this
language. The intermediate language is still subject to changes,
so this should be considered as experimental. Any feedback is
welcome!
The Salto project initially started as a partnership
between
Nomadic Labs
and Inria, and was funded
for 2 years by the
Tezos Foundation.
Since November 2024, the Salto project was granted a 1
year funding from the OCaml
Software Foundation.