Verifying Verifying Algorithm
Impression about Lean4
I’ve been studying Lean for several weeks as a programming language and as a proof assistant, I would like to share my experience.
My last Haskell project miso-css motivated me for the shift. It is a dependently typed HTML library that checks applicability of CSS classes to tags based on their ancestors and siblings and selectors.
After finishing the library, I realized that no tool exists for library verification, due to its core logic sits in type families. Verification would be the next logical step for such a library. After researching an alternative implementation language, I settled on Lean.
I was pleasantly surprised by the fact that Lean4 is a true functional PROGRAMMING language, until then there was a bunch of superstitious about Lean in my head, such as it was a solely proof assistant (like Rocq).
I would describe Lean4 in a few Haskell terms as a Haskell minus laziness, minus linear types, minus STM, plus dependent types and GC from Python. Lean4 carries lot of Haskell traits - type classes (Num is split into smaller classes), pure functions, monads, IO, TH (macros), TH with IO under the hood (elab), Type Families (expressible in regular functions), Wasm Backend, Hoogle (Loogle), cabal (lake), string interpolation.
Besides the lack of laziness, Lean encourages writing total functions a way harder than Haskell does by default.
Technical drawbacks that looks temporal:
- size of an executable compiled with mathlib (a compulsory-voluntary dependency) is more than 100mb, but I remember days when GHC generated ELFs of comparable sizes.
- mathlib itself takes 8gb per lake (cabal) project, but .lake folder can be shared via a symlink
- nix support is bad, I wasn’t able to setup a flake environment for Lean projects and had to install Debian along with NixOS (lake cache can’t recognize its artifacts on NixOS and tries to rebuild everything from scratch)
- build system heavily relies on internet and practically unusable offline
What is new:
-
Haskell is recognized as a language which is good for building parsers, but there is no parser combinator library for building total parsers, and Lean has one.
-
the language server, that is embedded just into Lean, is a head taller than HLS. The language server is combined with a proof assistant. Even a regular developer can benefit from defining concrete theorems (ie without ForAll and Exists quantifiers) instead of unit tests, because they don’t require deep math background and elaborated proofs and get feedback instantly, and these tests can naturally coexist next to their code.
The proof assistant side is highly influenced by Rocq, but there is no need to type C-c C-l to get current proof context - it is updated automatically with text cursor position. Recently, I had to replace a key switch for C on my keyboard - big advantage in ergonomics.
A Lean feature that might look totally redundant to a Haskeller is the implicit coercions. There is a few type classes that allow “silent” conversion values of one type into another, thought the feature is often neutralized by the need to specify value type explicitly instead of explicit coerce function.
Verified Hello World
Since I started learning software verification I was looking for a practical, but very simple project for getting experience with the subject. Finally, I came up with Luhn algorithm, that is used for checking credit card numbers entered by the user. It turned out there was no a repo on the internet dedicated to such a goal.
Core lemmas are less than 100 lines.
Proving an Hunit Test-like theorem (without free variables) is trivial:
example : validateLuhnString "4022 0050 8738 5915" = true := by decide
example : validateLuhnString "4022 0000 8738 5915" = false := by decide
QuickCheck-like theorems require scratching head harder or asking aristotle for help.
encodeLuhnRev_correct checks that for any sequence of digits (not 100 arbitrary ones), encoding and checking functions stay in-sync.
theorem encodeLuhn_correct (l : List ℕ) :
luhnNumberCorrect (encodeLuhn l) = true := by ...
Following theorem checks that the predicate validating a card number can detect a typo in single digit in any position of arbitrary long number.
theorem luhnNumberCorrect_catches { n m : ℕ } { l₀ l₁ : List ℕ }
(hNneM : n ≠ m) (hn : n < 10) (hm : m < 10)
(h : luhnNumberCorrect (l₀ ++ n :: l₁)) :
¬ luhnNumberCorrect (l₀ ++ m :: l₁) := by ...