安全でない宣言

Lean の特異なマークとして、ユーザは unsafe とマークされた宣言を書くことができ、これによって通常であれば禁止されるようなものが許可されるようになります。例えば、Lean は次のような定義を許可しています：

  unsafe def y : Nat := y

安全でない宣言はエクスポートされず ¹、信頼される必要もなく、（ちなみに）たとえこのマークがついたものの中であったとしても証明にて使うことは許可されません。それでもこのマークによる安全でない宣言の許可は Lean ユーザにとって有益です。なぜなら、証明を生成するために使用されるもののそれ自体に対しておよびそれ自体が証明である必要がないコードを書く際に、より多くの自由をユーザに与えるからです。

このことについて aesop ライブラリは優れた実例を有しています。Aesop は自動化のフレームワークです；これはユーザが証明を生成することを補助します。このライブラリのある時点で、aesop の作者たちはシステムのある部分を表現するにあたって、ここで見られるように 相互に定義された帰納型を使うことが最適だと考えました。偶然にも、この帰納型のセットは Lean の理論で宣言されている型の中に1つ無効なものがあり、Lean のカーネルでは許可されないため unsafe とマークする必要があります。

それでもこの定義を unsafe の宣言として許可することは開発者とユーザのどちらにとっても有益です。aesop の開発者は、Lean を使ってこのライブラリを書くにあたり望むままにライブラリを書くことができますが、それにあたってメタプログラミングの DSL を呼び出すことなく（そして学ぶこともなく）、またカーネルを満足させるために抜け道を使う必要もありません。aesop のユーザも aesop による 証明を aesop 自体を検証する必要なくエクスポートし検証することができます。