(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.
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 is a partnership between Nomadic Labs and Inria, and is funded by the Tezos Foundation.