Understanding Liquid Types, Contracts and Formal Verification with Ada/SPARK
Fernando Oleo Blanco · ACM SIGAda Ada Letters · 2025
In C-like languages (C++, Rust, Go, Java, C#...) data is generally boiled down to one identifier (variable name) and the computer representation of the data (floats, ints, array, structs...). This method completely devoids the data from its actual, real world meaning and prevents reasoning and analysis beyond some of the most basic properties. In Ada and SPARK, data types are modeled as close as possible to their real world meaning. However, this is generally not enough, as types and the subprograms that operate on them need to be able to represent the nature and properties of the data beyond what is offered by the basic constructs available in Ada. In Ada 2012, type and subprogram annotations became available, allowing the programmer to describe the full set of properties of the data types. This allows programs to be much more accurate, less error prone and easier to understand and reason about. This technique is commonly known in other circles as liquid types and contracts. The following article will summarize the main ideas and concepts presented in the FOSDEM 2025 talk of the same name as the article.