Thinking Formally

Writing a formal model asks for a slightly different way of thinking about software. Just as developers work at writing "clear code", there are techniques that make a model easier for a machine to reason about, and easier for you to ask questions about.

IML is a pure language, and that is the point

IML is based on the pure subset of OCaml. It does not allow side effects: nothing a function does can change anything declared outside it. Every change a function makes to the world has to appear in its return value.

This is not a fundamental limitation on what you can model. Programs with side effects convert into state machine models where you carry the state through the code explicitly. This transformation is well established: it goes back to the work of Boyer and Moore on ACL2, and very complex systems have been encoded this way.

Three more properties shape how models are written:

Static types. IML is statically typed: a variable's type is fixed before the program runs and cannot change. Assigning None, then a string, then an integer to the same name is ordinary in Python. In IML it is not possible. If a model adds an integer to a string, ImandraX returns an error rather than a coercion. This is itself a form of logical reasoning, and it is why type information extracted from the source language matters so much when building a model.

Recursion instead of loops. while and for loops become recursive function calls. This is not stylistic: reasoning about iteration ultimately requires reasoning by induction, and writing the iteration as recursion makes the inductive step visible. See induction control for what to do when the automatic choice is wrong.

State machines are usually infinite. A state type can contain lists and records as well as numbers, so the state space is typically unbounded rather than a finite set of named states. This is what makes the technique useful for real systems: a stock exchange model can carry an incoming order stream as a list that a top-level step function folds over.

What should you model? A question about abstraction

The useful question is not "what code can CodeLogician handle" but "what should I model, and at what level of detail". Almost any executable program can be modelled in ImandraX; whether you should depends on what you want to know.

Take a C routine that sorts a list of integers, with the usual memory allocation. Two different questions:

  • Does it ever dereference deallocated memory? Answering this needs a faithful model of the memory manager and the semantics of the relevant operations.
  • Is the returned list sorted? This needs no model of memory at all.

The second question sits at a higher level of abstraction than the first. What you want to reason about determines the abstraction level, which in turn determines the shape of the model. Three rough bands:

High-level. Domain-specific languages representing complex processes or systems. A program in such a language translates to IML with high compression. Imandra's own Imandra Protocol Language (IPL), used to model symbolic state transition systems such as a complex trading API, runs at roughly 1:10, with one line of IPL becoming ten of IML. For this band we would not reach for CodeLogician; the better move is a DSL that compiles to ImandraX directly. Reasoning here concerns non-trivial state transitions and validation of rich structured input conditioned on current state.

Mid-level. Application code, meaning most of the software most people work on day to day. This is the sweet spot: source programs encode into models directly, with no DSL in between.

Low-level. Instruction-level code. An excellent application of ImandraX, but outside what CodeLogician does. Analysis here means building a virtual machine: a memory model, and a CPU that gives the instructions meaning. Imandra built the first formal model of the Ethereum Virtual Machine this way, which required an executable model of the VM itself, not just a list of instruction definitions. Handed a sequence of low-level instructions with no such machine available, CodeLogician has nothing to give the instructions meaning with.

Reasoning about code you can't see

Almost no code avoids third-party libraries and services, and running such code means assuming those dependencies behave in a certain way. Very few developers using a pseudo-random number generator have read its implementation and convinced themselves it behaves as documented. Without assumptions like this, software development would not scale.

When testing, the usual response is mocking: small approximations of the outside world, so results are reproducible. Formalisation uses the same idea, made explicit. There is a second reason to approximate, too: some things resist reasoning not because they are external, but because they are mathematically hard to handle directly.

This is a large enough topic to have its own page: Handle external dependencies.

Where to go next

Previous← Why Logic-First
NextAutoformalization →