Lean - Can we Trust the Trust Engine?

The de Bruin principle - it's all in the Kernel

Once upon a time, in the 1960s, a computer scientist called de Bruijn build a system called Automath. His full name as Nicolaas Govert de Bruijn. It incorporated ideas such as dependent types to make it work.

We call him here a computer scientist, but he can equally be called a mathematician, having made contributions to number theory, analysis, combinatorics and logic, and served as Professor of Mathematics at the University of Amsterdam.

One of the things he studied were sequences now known as de Bruijn sequences. Polish programmer Andrzej Trybulec's Mizar system was influenced by Automath.

De Bruijn came up with the idea of creating a kernel separate from the rest of his system.  This kernel is correctness-validation component of the system - the "rule-checker" if you will. It is like the part of a chess computer that validates legal moves - rather than makes smart moves.

Keeping the kernel separate is known as the de Bruijn principle, joining lots of other artefacts attached to his name (such as the de Bruijn-Newman constant, which is closely associated with the Riemann hypothesis).

What underlying logic to use for the Kernel?

"First order" logic, augmented with axioms of set theory, can serve as a good starting point for a theorem prover/correctness checker.   This approach results in a small kernel but lots of coding for complex mathematics. More complex underlying systems are available, including Higher Order Logic (HOL) and Calculus of Inductive Constructions (CIC). Lean uses the latter, or at least features of the latter, to increase expressivity and make programming easier. Features used include proof irrelevance, quotients and nested inductive types.

Taking one example: proof irrelevance is the principle that given a proposition and any two proofs of the same, the two proofs are (considered) equal. This simplifies type theoretic reasoning.

The result is that Lean has a kernel that is much smaller than Lean itself but verifying it is not trivial.

lean4lean and the "multiple kernel" principle

Creator of Lean, L. de Moura, has advocated the "multiple kernel" principle, strengthening the de Bruijn principle by supporting multiple independent kernels.  Lean 3 thus had three independent kernels, one in Lean, one in Haskell and one in Scala (trepplein). Lean 4 invalidated these kernels. Nanoda, an independent kernel in Rust, was thus commissioned together with procedures to write more kernels.

lean4lean was started by Mario Carneiro, an implementation of Lean in Lean which includes an independent kernel.  Efforts are ongoing to verify kernel correctness.

Latest Haskell Compilers

A good, up-to-date Haskell compiler is the GHC. 

Unlike earlier compilers e.g. Hugs, GHC has support for concurrency and parallelism, including Software Transactional Memory.

There are some language extensions available, including support for the FFI, or Foreign Function interface, which is enabled by default.

The latest Haskell Report on which the current version of GHC is based on is Haskell 2010.

One unfortunate fact about Haskell is poorly maintained external libraries.

Lambda Calculus and System F

The lambda calculus is a theory that treats functions as formulas or expressions. 

Arithmetic is another example of a language of expressions.  

In arithmetic, you have variables (x,y,z..), numbers (1,2,3...) and operators (+, - ...). x+y then denotes the output of applying the addition operator to x and y and this can be extended to more complicated expressions. 

Lambda calculus extends this concept to functions. 

If we define a function f mapping x to x squared; then consider A = f(10); then in the lambda calculus we simply write A = (lambda x. x^2)(10). The expression (lambda x. x^squared) stands for the function that maps x to x squared rather than the statement that x is mapped to x squared.

One advantage of the lambda calculus, is it allows us to easily consider higher-order functions, i.e. functions with functions as inputs and/or outputs. 

An example is the expression f maps to f.f which takes the function f and applies it to the function f, the composition of f with itself. In lambda notation we write (lambda x.f(f(x)) and the operation that maps f to f composed with itself is (lambda f . lambda x. f(f(x)). You can see this is easy to extend to triple composition, and so on.

Technically speaking, lambda calculus is Turing-complete, that is, it is a universal model of computation that can be used to simulate any Turing machine.

Now lambda calculus can be typed or untyped, typed is more restrictive - we say it is weaker than untyped lambda calculus. In untyped lambda calculus we are flexible about domains and codomains. For typed calculus we have simply-typed - where we specify the type of every expression and polymorphically typed, where we have types of a specific form X->X but we don't specify the type.

System F is a form of polymorphic lambda calculus.

System F formalizes parametric polymorphism in languages. In so doing, it forms a theoretical basis for languages like ML and Haskell. 

System F was discovered independently by logician Jean-Yves Girard (1972) working in proof theory, and computer scientist John C Reynolds, who held positions at Edinburgh University, Imperial College and Carnegie Mellon.

The ideas aforementioned stemmed from interest and investigation in the 1930s into what does it mean for a function to be "computable" - in other words, have results derivable using (in principle) pencil and paper only.

Haskell Vs Erlang

Haskell and Erlang are both functional programming languages. Erlang has multithreading built in and has been historically more industry focused with its roots in the telecoms industry. F# is another functional language that supports concurrency through the async computation expression.