The IML Language

The Imandra Modelling Language (IML) is the language at the heart of ImandraX. It is a pure, higher-order subset of OCaml that simultaneously serves three roles: a programming language you can execute, a formal logic for stating properties and specifications, and the foundation of a reasoning engine for constructing proofs with a very high degree of automation.

When you write an IML function, you're writing real, executable code. But you're also writing a mathematical definition that ImandraX can analyze, prove properties about, and synthesize counterexamples for. Moreover, proofs and tactics are also expressed in IML — users compose proofs using a rich tactic language built into ImandraX, and the system is extensible: users can define new tactics for domain-specific proof automation, and as they verify their systems they build up libraries of definitions, lemmas, and tactics that teach ImandraX how to reason effectively in their problem area.

What IML looks like

If you know OCaml, Haskell, F#, or similar functional languages, IML will feel immediately familiar:

(* Types *)
type color = Red | Green | Blue
 
type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree
 
(* Functions *)
let rec size = function
  | Leaf _ -> 1
  | Node (l, r) -> size l + size r + 1
 
(* Theorems *)
theorem size_positive t =
  size t >= 1
[@@by auto]

What makes IML special

IML is not arbitrary OCaml. It is a carefully chosen subset that guarantees every definition can be reasoned about formally:

  • Pure — No side effects, no mutation, no I/O within the logic. This is no real restriction from a modelling perspective — impure aspects of a system can always be moved into the computational model, with state passed around explicitly (monadically)
  • Total — Every function must terminate on every input
  • Higher-order — Functions can take and return other functions
  • Specializable — Higher-order definitions can always be reduced to first-order form for automated reasoning

These restrictions ensure logical consistency: you can never accidentally "prove" something false. The theoretical foundation is a computational fragment of higher-order logic (HOL) extended with transfinite induction up to ε₀.

In this section

Previous← VS Code Guide
NextBasics →