i2: A language for verified reasoning

NB: i2 is nothing more than a very rough draft right now. It is meant to express our ideas and thereby stimulate thought, discussion and the formation of a small community through which, we hope, it will become a useful tool for the average mathematician.

i2 is a language designed to make formal verification easy. While there has been great progress in this area in recent years, in most cases, formal verification remains an arcane art inaccessible to "the unitiated". We hope to change this by presenting a small, orthogonal feature set in a simple syntax that can be learned in an afternoon.

tmpl thm1(m nat, n nat) { !eq(m, n) ==> !eq(succ(m), succ(n)) } {
	eq(succ(m), succ(n))
==> { injectivity(m, n) }
	eq(m, n);
};

That is, for all natural numbers $m, n$ we have $$ (m \ne n) \implies (\text{succ}(m) \ne \text{succ}(n)). $$ However, the above code will not verify on its own, since it makes reference to many undefined objects. The axioms that power it are as follows:

/* eq: Equality. i2 currently supports only logical operators and funtional
 * application, because we haven't yet found a simple way of introducing
 * higher-order operators (such as the equals-sign). */
@func eq(x any, y any) bool;

/* nat: A natural number. */
@func nat(x any) bool;

/* Types and predicates are the same thing in i2: boolean-valued functions.
 * However, we do permit the syntax
 * 	x P
 * to indicate "x is of type P", i.e. that P(x) is true.
 * The `@' means "axiomatic": we are merely postulating the existence of the 
 * types rather than providing an expression to which it evaluates. */

/* 1 is a natural number. */
term 1 nat;

/* This is like a global constant declaration. It occupies the place of Peano's
 * first axiom that 1 ∈ N. */

/* succ: For each x there exists exactly one natural number, called the
 * successor of x. */
@func succ(x nat) nat;

/* In other words: we postulate the existence of the succ(x) for every natural
 * number x. */

/* injectivity: If succ(x) == succ(y) then x == y. */ 
@tmpl injectivity(x nat, y nat) { eq(succ(x), succ(y)) ==> eq(x, y) };

/* The `@' here now indicates that the statement given in the template is
 * axiomatic (to be accepted by the verifier without proof). */

With three additional axioms, we are in a position to make our first inductive proof.

/* succ_notone: We always have succ(x) != 1. */
@tmpl succ_notone(x nat) { !eq(succ(x), 1) };

/* induction: The axiom of induction. */
@tmpl induction(P func(nat) bool) {
	P(1) && (x nat) { P(x) ==> P(succ(x)) }
==> (x nat) { P(x) }
};

/* application: This is a bit of a red-herring, present because i2's logical
 * kernel currently has a very superficial understanding of quantification. */
@tmpl application(P func(nat) bool, w nat) {
	(x nat) { P(x) } ==> P(w)
};

And now for the proof, which is of the theorem that for all natural numbers $x$ we have $ succ(x) \ne x. $

tmpl thm2(x nat) { !eq(succ(x), x) } {
base:	this(1)
<== { succ_notone(1) }
	true;

induct: (x nat) {
		this(x)
	==> { thm1(succ(x), x) }
		this(succ(x))
	};

	base && induct
==> { induction(this) }
	(x nat) { this(x) }
==> { application(this, x) }	
	this(x);
};

There are many mouthfuls in these two examples, and indeed, many things that need to change, some that we can see (like the issue with quantification) and some that we cannot (but you may).

Getting started

There are two ways of working with i2. If you are comfortable working from the command line:

git clone https://git.sr.ht/~lbnz/i2
cd i2 && make
./bin/i2 examples/landau/addition-induction.i2

We are also building i2forge in order to facilitate the use of i2 by non-programmers. i2forge is currently running in closed alpha while we iron out the kinks. If you are interested in joining the alpha, see here. (Note: i2forge is not an open source project, unlike i2.)

Getting started

Community