I recently learnt about the Lean language at an event at IISC. It's a language used not just for writing programs but proving that they are correct.

So what does it mean to "prove" something is correct exactly. George Polya mentions this in his book "How to solve it". Verification is the fourth step of a coming up with a solution. It means that can you prove that the solution you have come up works "reasonably" well. Even when the way at which you look at the problem changes. For example, think of the simple Pythagoras theorem. One way to verify is to check is to you multiply the sides by a particular number to make a new triangle. Then the third side also has to be multiplied by that number to get the third side of the second triangle.

This is quite an interesting step actually. It shows to you, not just that you were right in that one scenario in your head. You can twist and turn around the problem, and still what you've come up with is correct. It cements your understanding of the problem. You are not just flailing in the air. Clutching to your solutions with dear hands, because you had so much trouble coming up with it. It is correct in many ways. Someone else could have taken an alternate route, holding the orb of the problem in a different light. But you've both crash landed to the same spot.

Let's look at an orb shall we? Quicksort is a sorting algorithm most computer science people learn fairly early on. Think of it like taking a row of people in front of you. You have to sort them by height. Currently, they are all over the place. So you take the first person, and you bring her out. Her name is Pivot (Her parents were a bit strange, we don't talk about it). Then you keep moving ahead. Any person who is shorter than her (doesn't matter the order), you place in front of her. Any person taller than her, you place them behind her. Then, you repeat this entire process again, considering all the people in front of her as an entirely new batch. And for all the people behind her, again as a new batch. Rinse, repeat.

In a 'normal' programming language, this is usually written like a 'for loop'. Most first year university students would write the program that way.

def partition(arr, low, high):
    pivot = arr[high]
    i = low - 1
    for j in range(low, high):
        if arr[j] <= pivot:
            i += 1
            arr[i], arr[j] = arr[j], arr[i]
    arr[i + 1], arr[high] = arr[high], arr[i + 1]
    return i + 1

def quick_sort(arr, low, high):
    if low < high:
        p = partition(arr, low, high)
        quick_sort(arr, low, p - 1)
        quick_sort(arr, p + 1, high)

arr = [1, 7, 4, 1, 10, 9, -2]
quick_sort(arr, 0, len(arr) - 1)
print(arr)

In this approach, you are going through each element, checking it's position, what is larger and smaller. And then based on it's value, switching places with other elements using the positions. Repeat till you get it right.

Lean, by contrast, is a functional programming language. It looks VERY similar to Haskell. This is a piece of Lean code for example for quicksort.

def quickSort : List α → List α

| [] => []

| pivot :: l =>

(quickSort (smaller pivot l)) ++ pivot :: (quickSort (larger pivot l))

-- termination_by l => l.length --ignore this for now

This is a classic program I use when introducing people to Haskell too. But there are no loops in functional programming languages. We take the first element of the provided list. Then we put all the elements of the list smaller it before it, and all the ones bigger than it after it. Then for the remaining elements of the left and right side, you repeat the same process. This is a different way of doing this. Approach (1) is way more common. But this is a different way of thinking about the problem. And it expresses the solution of the problem quite beautifully.

There is also some Lispy stuff in Lean. Metaprogramming effectively. You can extend the language if you want. Writing DSLs (Domain specific Languages) in Lean is super easy. In simple words, you have more control over the order of execution of code. More than you would have in say Java or Python (conditions applied). A simple analogy is automatic vs manual cars. You have even more control actually. In lisp it's like you can change the car internals as you are driving it. Very cool stuff. A different way of thinking about the problem.

But these are the parts I am very familiar with. In fact, the creator of the language, Leo de moura (along with others), built it with these features in mind. But then all this other stuff comes in.

Theorems?

theorem irrational_sqrt_two : Irrational (√2) := by
  simpa using Nat.prime_two.irrational_sqrt

Axioms?

axiom ::= ...
    | axiom declId [declSig]

Tactics and proofs and lemmas? Some within structures?

structure Voter extends Person where
    votedId: Nat
    is_voting_eligible: 18 <= age := by grind -- this is the tactic/proof part
    deriving Repr, DecidableEq

What's going on? This is stuff from college I don't remember. Let us blame the pandemic for that, shall we. Regardless, it's not really well taught at Indian Universities at least. Your standard engineering course will do a cursory glance over this. But I could recall that axioms are effectively the smallest unit in maths. Something which acts as the ground from which we build up systems. Theorems, proofs etc all emerge from axioms.

Official Definitions:

An Axiom (or Postulate) is a starting rule we accept as true without proof

A Theorem is a major result (proved using axioms and earlier results)

A Lemma is a result proved mainly to help prove another theorem

And these systems emerge from a set of axioms that CANNOT be proven. They are assumed to be true. A leap of faith if you will. We all know this is true. Can't go below this level. There is a lot more behind this that I am unqualified to cover, but there are some reasons why this is the case.

So these theorems are BUILT-IN in the Lean compiler basically. 3 foundational math axioms, 1 sorry axiom, and 3 kernel axioms 1. We hold these truths to be self evident. Programming languages all come with their own styles. But this is some other dimension of style that I haven't come across. A language which says no, there are AXIOMS in this world. This is math territory. This is true. Make your theorems on top of this. It is pragmatic also, it allows you to write your own axioms. Which is also crazy. But generally it is a good practice to not play God.

It means that when you build theorems, you can then prove them. And build systems that can work on the basis of those theorems. Each theorem is a template of sorts. A template can say look I am copying everything from that template, and then I'll add my own stuff too. Or templates can relate to one another. A class can say look, for this part of my structure, look at this other template. And this holds true for theorems.

For example you can say in Lean, look, I am modelling the Kepler laws of motion. These are the theorems, proofs etc. And then you build your systems around that. Later, if you want you can proof newton's laws of motion. And then you can prove that Keplers laws of motion are derived from newtons. So now your system works provided Newtons laws are true. And the KERNEL. The innermost part of the language assumes this when you write this code. It cares that you have defined these theorems. And it will respect that. Writing an axiom means you are telling the kernel, hey this thing is almost God level true. And the innermost part of the language understands this.

This is what I love about programming. Being introduced to new ways of thinking. This is not something I ever thought a programming language would ever consider. How do you prove things are correct? How long do you keep turning the orb. Polya talked about this as well. He was writing to teach students. To him, it was a matter of the student becoming confident in the correctness of the solution. In most real world production systems, this is done by "testing" the program. But mathematicians like going a level above of course. How can you abstract even this? There are so many ways to model that. It forces you to get a bird's eye view of the problem. Turn it around, does it still work like you thought you would?

There is still so much I don't know about this. But it's nice to find a new way of thinking about things. Even just for a little while.

Refs

1. Lean Docs
   
2. Math is Fun
   
3. George Polya's How to solve it
   
4. Quicksort in Python is from GFG of all things

1. I(wrongly) wrote 11 axioms are present in Lean without verifying it. The corrected figure is above.

Post Notes

1. There is tactic called sorry in Lean. Very funny.
   
2. A good way to look at this for now is to just think of it as Haskell with richer data types. I am scared of the math theory, but as one of my teachers said "You people are scared of the wrong things." Go into it thinking, even if it's out of your league, you'll learn something. If you're not in over your head, how do you know how tall you are?