Lean言語が「完璧化可能」な理由を解説

Alok Singh氏が個人ブログで、Lean言語が他のプログラミング言語より優れている理由を詳しく説明した。氏は40のプログラミング言語を挙げた上で、Leanが最も優秀だと主張している。その理由として「完璧化可能（perfectable）」であることを挙げた。

Lean言語の特徴は、言語内で自身の性質や証明を記述できることだ。例えば「常に5を返す関数」について、その性質を定理として証明し、コンパイル時に検証できる。これは依存型システムと定理証明インフラストラクチャによって実現されている。

氏は多くの言語が後から型システムを追加する傾向にあることを指摘した。PHP 7.4やPythonの型アノテーション、TypeScriptやRustの普及などがその例だ。C++のテンプレートやRustのconst化も、コンパイル時計算への需要を示している。

Leanのもう一つの強みはメタプログラミング機能だ。カスタム構文を定義でき、例として三目並べのボード記法を実装できることを示した。この機能により、ドメイン固有の記法を自然に統合できる。氏はこれらの特徴により、Leanが真に「完璧化可能」な言語だと結論づけている。