Differences from OCaml

IML is a subset of OCaml — not all of OCaml. This page explains what's excluded and why. The restrictions exist to ensure that every IML definition is a conservative extension of the logic, maintaining soundness and consistency.

Not in IML: Mutation

OCaml has mutable references, mutable record fields, and arrays with in-place update. None of these are in IML.

(* OCaml — NOT valid IML *)
let counter = ref 0
let increment () = counter := !counter + 1

Why: Mutable state makes it impossible to reason equationally about programs. If f x can return different values at different times, the equation f x = f x isn't guaranteed. IML functions are mathematical functions — same input, same output, always.

Not in IML: Exceptions

OCaml's exception mechanism is not available in IML.

(* OCaml — NOT valid IML *)
let safe_divide x y =
  if y = 0 then raise Division_by_zero
  else x / y

Why: Exceptions introduce non-local control flow that bypasses the normal evaluation model. In IML, every expression evaluates to a value. Use option instead:

(* IML — use option for fallible operations *)
let safe_divide x y =
  if y = 0 then None
  else Some (x / y)

Not in IML: Side effects

No I/O, printing, file access, network calls, or any other side effects in logic mode.

(* OCaml — NOT valid IML in logic mode *)
let log msg = print_endline msg

Why: Side effects are not observable in the logic. A function that prints and returns 42 is logically equivalent to one that just returns 42 with respect to its return value, but the two programs behave differently in practice. If you need side effects, extract your verified code to OCaml and add them there (see Evaluation & Extraction).

Not in IML: Non-termination

All recursive functions in IML must terminate on all inputs.

(* OCaml — NOT valid IML *)
let rec loop () = loop ()
 
(* OCaml — NOT valid IML (might not terminate for negative n) *)
let rec countdown n =
  if n = 0 then 0
  else countdown (n - 1)

Why: Non-terminating functions can derive contradictions. If f x = f x + 1 were accepted, subtracting f x from both sides gives 0 = 1. See Termination for details on how ImandraX proves termination.

Fix: Use <= instead of = to handle negative inputs:

(* Valid IML — terminates for all n *)
let rec countdown n =
  if n <= 0 then 0
  else countdown (n - 1)

Not in IML: Objects and classes

OCaml's object system is not part of IML.

Why: IML's type system is based on algebraic datatypes and records, which have well-defined induction principles. Objects with inheritance and dynamic dispatch don't have clean inductive structure.

Not in IML: Imperative control flow

while loops, for loops, and sequential composition (; for side-effecting statements) are not in IML.

Why: These constructs are inherently imperative. In IML, use recursion instead of loops and let ... in instead of sequential composition.

Not in IML: First-class modules and functors

OCaml's first-class modules and functors are not supported in IML.

Why: These features interact with the type system in ways that complicate the logical semantics. Use regular modules for namespace organization.

What IS in IML

Despite these restrictions, IML is a rich language:

• Algebraic datatypes with pattern matching
• Records with functional update
• Polymorphic types and functions
• Higher-order functions (with specialization)
• Local bindings (let ... in)
• Tuples, lists, options, and other standard types
• Full integer and rational arithmetic
• String operations
• Module system for code organization
• Import system for multi-file projects

The restrictions are precisely those needed to ensure that every IML program has a clear mathematical meaning that ImandraX can reason about.