I was selected to attend the LeanLang Summer School conducted by Emergence AI. This was a first-of-its-kind attempt to bring Lean to the masses, both to students and industry professionals. Titled "LeanLang for Programming", it brought in some of the best researchers, including Siddhartha Gadgil, who is one of the foremost proponents of Lean in India, along with Prof. Ilya Sergey, who pioneered multi-modal theorem proving in Lean. Emergence also did a great job encouraging students, by sponsoring stay at a 4-star hotel!

The first day experience

The day began with an introductory session by Prof. Siddhartha Gadgil, on the fundamentals of Lean. Although most of this was familiar to me, it was a nice memory refresh. His method of presenting concepts was also worth emulating. Subsequently, there was a lab session, where we could try out various exercises as given in the LeanLangur repository. It was a nice experience revisiting some of the concepts from CS6225

Hoare Logic by Prof. Deepak D'Souza

The first lecture of the day offered a theoretical look into Hoare Logic, focusing on Inductive Annotation as presented by Floyd. The slides are linked here. The idea is to prove that a postcondition holds given a pre-condition about the state of the program and various statements of the program executed as per their semantics. A simple language could be considered - such as x := e, if b then S else T and while b do S, along with the sequencing operator ;.

In order to prove statements, two kinds of annotations are useful at each program point -

1. Adequacy : To show that the Precondition implies the annotation at the first statement \(A_1\), as well as the annotation at the last statement \(A_n\) implies the postcondition
2. Induction : To show that subsequent annotations imply each other as per the control flow graph of the program. In mathematical notation, \(A_i \land [S_i] \Rightarrow A'_{i+1}\).

An illustrative example is shown in the below figure. .

The talk also discussed the soundness and completeness of this logic system under the condition that the weakest precondition is expressible in the language \(L\).

Velvet by Prof. Ilya Sergey

The second talk by Prof. Ilya extended the ideas of hoare logic built by the previous talk. It extended the theory of SMT solving and hoare logic to prove imperative programs, similar to what we write in a small imperative language. A simple example is

method insertionSort
  (mut arr: Array Int) return (u: Unit)
  require 1 ≤ arr.size
  ensures ∀ i j, 0 ≤ i ∧ i ≤ j ∧ j < arr.size → arr[i]! ≤ arr[j]!
  ensures arr.toMultiset = arrOld.toMultiset
  do
    let mut n := 1
    while n ≠ arr.size
    invariant arr.size = arrOld.size
    invariant 1 ≤ n ∧ n ≤ arr.size
    invariant ∀ i j, 0 ≤ i ∧ i < j ∧ j ≤ n - 1 → arr[i]! ≤ arr[j]!
    invariant arr.toMultiset = arrOld.toMultiset
    -- decreasing arr.size - n
    do
      let mut mind := n
      while mind ≠ 0
      invariant arr.size = arrOld.size
      invariant mind ≤ n
      invariant ∀ i j, 0 ≤ i ∧ i < j ∧ j ≤ n ∧ j ≠ mind → arr[i]! ≤ arr[j]!
      invariant arr.toMultiset = arrOld.toMultiset
      -- decreasing mind
      do
        if arr[mind]! < arr[mind - 1]! then
          swap! arr[mind]! arr[mind - 1]!
        mind := mind - 1
      n := n + 1 -- try commenting this out for termination
    return

This program uses monads to mimic an imperative language within lean to perform insertion sort. The syntax is similar to Dafny. Velvet comes with handy SMT-based tactics to prove such programs, as well as a QuickCheck-based counterexample generator.

It also allows for angelic and demonic randomness, which represent the existential and the forall (adversarial) cases, respectively.