システム · 設計、どのリリースにも入っていません
LSPE
ビルドは、プログラムについての判断の集まりです。LSPE はコンパイラにその判断の説明を求めます。 まず各判断の出所を自分で探し、見つからなければ記録に残る質問としてあなたに渡し、そのやり取りを 成果物に書き込みます。プログラムが正しいことは約束しません。約束するのは 黙って通した例外は一つもないということです。
設計であって、ダウンロードできるものではありません
2026-10-18 の時点で、LSPE は設計です。どのリリースにも入っておらず、インストールできるものも
なく、このページにはいつ出るかの日付も書かれていません。設計そのものはリポジトリの
docs/262 にあります — 他の番号付き設計文書と同じく中国語で、このプロジェクトは
計画を公開の issue トラッカーではなくそこに置いています。
以下は、この設計が何のためで、何を主張しないかです。有効にできる機能の発表ではありません。
設計は約束ではありません。 できないと分かっていることが二つあり、設計はそれを 回避せずに書き留めます。プログラムに欠陥がないことを証明できるコンパイラはなく、自分が答えられない 問いのすべてに答えられるコンパイラもありません。以下のすべてはこの二つに形づくられています。
判断のたびに一枚のレシート
今のコンパイラが返すのは一位の情報だけです。受け入れたか、拒否したか。理由はコンパイラの内側に 残り、「受け入れた」に至るまでに置いた仮定は、あなたが確かめられる場所には書かれていません。
LSPE は記録を足します。証明できなかったのに通したとき、成果物はその判断がどれで、どんな証拠に 支えられ、人が答えたのなら誰が答えたかを書き留めます。成果物が持つのはその記録のハッシュで、 導出木は成果物の外に並べて置かれるので、成果物はそれで大きくなりません。
これは「欠陥がない」ではありません。 プログラムに欠陥がないかはコンパイラには 判定できません。例外がすべて書き留められたかは判定できます。前者は決定不能で、後者はプロセスの 性質であり、コンパイラを信じない人でも事後にオフラインで確かめられます。
四つの部品
LSPE は四つの部品で、ひとつの空間の上で働きます。あるユニットで判断が下された地点、その地点が 負う義務、それを支える証拠、そして各枠がどうなったかの記録です。五つ目の検査器ではありません。 検査器はみな元の場所に残ります。
問いただす者
コンパイラは判定者であることをやめません。ある判断を受け入れる前に、その出所を探し、 反例を作ろうとし、もう一つの実装に突き合わせます。三つとも失敗すれば穴があります — そしてそれは自分に穴があると言うのであって、あなたのコードが悪いとは言いません。
問い返す者
穴は、選択肢・既定値・それぞれの結果を伴う問いになります。あなたの答えは記録されます。 記録されない先送りはそれ自体がコンパイルエラーです — 「ここは怪しいが理由を言えない」が 誰かの頭の中だけに住む知識ではなくなります。
警察 LSPC
ビルドの前に勘定書を渡します。これから受け入れる残余リスクはどれか、一族ごとに一行、 その一族が成り立たないと何が起きるか付きで。既定では止めません。直したいものは直し、 残すものは残す。残したことが記録されます。
台帳
他の安全部品が出した判定 — 回収の梯子、メモリ安全の段階、能力域、所有権 — が 一冊の台帳に集まります。どの部品も置き換えず、名前も変えません。台帳は、それらの判定を 並べて読み、突き合わせられる場所です。
立証責任の向きが変わる
ふつうのコンパイラはプログラムの外に立ち、結果だけを告げます。LSPE は取引の内側に座ります。 根拠を名指しし、置いた仮定に値段を付け、レシートを渡します。証明できないとき、 「あなたのコードが間違っている」とは言えません。「私の証明にはここに穴がある」と言わなければ なりません。前者はあなたについての主張、後者はコンパイラについての主張で、この二つは意図して 分けられています。
この分離には費用がかかり、設計はそれを払います。問いただす者は型の置換のたびにログを残し、 置換のあとで義務を証明し直します。Rust 自身の記録にも、まさにその形の健全性の欠陥があります — 置換の前に成り立っていた検査が、置換のあとにもう一度走らなかった、というものです。 「出所はあるか」だけを問うコンパイラには捕まえられません。出所はそのとき存在し、そして 期限切れになっていたからです。
店員は権威ではありません。 意味論は標準と各コンポーネントに属します。 LSPE は判断を記録し値段を付けるだけで、何が真かを決めはしません。
しないこと
メモリの誤りをもっと見つけるわけではありません
見つけるのは、出所のない放行と、期限切れの証拠です。そういう放行がないプログラムでも、 間違っていることはあります。
プログラムを安全にするわけではありません
残余リスクを黙って受け入れることを不可能にします。これは二つの別の数で、設計は 一方を他方と引き換えにせず、分けて持ちます。
検査器を置き換えません
回収の梯子、メモリ安全の段階、能力域、所有権は、それぞれの名前・持ち主・判据を保ちます。 LSPE はその判定を読むだけです。
検査を減らす手段ではありません
監査を閉じるのは、あなたが署名する記録された選択であって、検査を消すスイッチではありません。 検査はどちらでも走り続けます。変わるのは、結果が書き留められるかどうかです。