TL;DR
純粋関数型プログラミング言語であり、定理証明支援系でもある。仕様と証明を、プログラムと同じ言語で書ける。
なぜ必要か
依存型を使って厳密な仕様を書き、プログラムがその仕様を満たすことを証明できる。テストと違い、1 つの証明でテストしていない入力も含むすべての入力に対する正しさを保証できる。数学者向けには、形式化された数学ライブラリ Mathlib がある。Cedar の形式検証にも Lean が使われている。
仕組み
ツールチェーンは、バージョン管理ツールの elan で入れる。パッケージ管理ツールの lake も elan に付いてくる。
# elan を入れる
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
# elan 自体を更新する
elan self update
# 最新の安定版を入れて有効にする
elan default leanprover/lean4:stable.zshrc でパスを通す。
export PATH=$PATH:$HOME/.elan/binVisual Studio Code の拡張を入れても、必要なものが入るようである。ブラウザで試すなら Playground がある。パッケージは Reservoir で探せる。
自分の理解
環境構築を IDE に依存させるのは気持ち悪いので、elan で手動で入れることにした。