New to Rocq? Read this section.
SLOT is a fully formally-verified model checker that can verify safety properties of programs written in “SLOTLang”, a shallow-embedded DSL inspired by Erlang.
SLOTLang is an actor-based language capable of performing input-output operations in a simulated environment. It extends plain Gallina[fn:1] with 4 primitives:
- spawn: spawn a child process
- do: perform I/O operation
- yield: NOP, interrupts the computation
- die: terminate the process
They allow to write programs that (if you squint hard enough) resemble Erlang:
Let prog : prog_t h True :=
spawn c1 <- child1;
c1 ! 1;
spawn c2 <- child2;
c2 ! false;
die.I/O operations are non-deterministic: they can fail, produce different results for the same input or block. This is sufficient, for example, to model network with packet loss and reordering. SLOT verification is total: it considers every possible outcome of such operations.
I/O is implemented via composable effect handlers. This makes SLOT extendable: it is possible for the user to implement custom effects, and mix and match them with the existing ones.
This section is meant as a soft encouragement for programmers unfamiliar with Rocq to research and study it. For a full tutorial please check a free e-book Software Foundations.
While Rocq (formerly known as Coq) features a baroque syntax inspired by mathematical proofs, that may look rather intimidating, the good news is that under the hood it is merely a functional programming language with an extremely expressive type system and unparalleled meta-programming facilities. It does not contain any special magic, just functions and data types cleverly mapped to various mathematical concepts. So, if you are, say, an Erlang programmer, you already have about 70% of the basics covered.
Using functional programming to prove mathematical theorems is possible thanks to Curry-Howard correspondence. It’s an observation that application of a function to arguments is similar to modus ponens logical inference rule: the arguments can be thought as hypotheses, the return type of the function as a theorem, and body of the function as a proof of the theorem.
Please note that this similarity is all but superficial,
and most programming languages fail miserably as theorem provers:
to serve as proofs,
functions must be pure and total,
i.e. they must return a value for every possible input.
Regular programming languages allow functions to throw exceptions,
perform unsafe types casts and/or loop infinitely.
Such behaviors allow to “prove” false statements,
which is disastrous from the logic perspective due to ex falso quodlibet principle:
a formal system containing even a single logical contradiction allows to prove any statement whatsoever:
given statements A and ¬A,
A → A ∨ B, and ¬ A ∧ (A ∨ B) → B,
where B is any statement.
Rocq is one of a few exceptions, because at its core it enforces totality of the functions, often at the cost of other features, like I/O or Turing completeness.
SLOT framework bridges the gap between the two worlds: it simulates I/O via logical statements describing mutations of the state space, and allows for infinitely running programs, as long as they either do I/O or yield.
While code in this repository may look nothing like, say, Erlang, it’s all just functional programming in disguise.
Fancy syntax like
Lemma foo : forall (a b : nat), a + b = b + a.
Proof.
intros.
induction a.
- auto.
- simpl. now rewrite IHa, plus_n_Sm.
Qed.is translated to “normal” FP language as a definition of function foo with type
fun a b => eq (a + b) (b + a).
Body of this function defined with the help of Rocq’s meta-programming language called Ltac:
intros. command prompts Rocq to create an anonymous function with arguments guessed from the context,
induction a. calls a special function associated with the type nat,
auto. means “vibe-code whatever term to fill the gap”, etc.
[fn:1] Gallina is the specification language of Rocq