要約する内容はありません。
Rustの可変エイリアスと型検証に関するいくつかのノート (graydon2.dreamwidth.org) 1 ポイント 投稿者 GN⁺ 2024-05-17 | 1件のコメント | WhatsAppで共有 要約する内容はありません。 関連記事 Ante: 借用検査と参照カウントを組み合わせる新しい方式 1 ポイント · 1件のコメント · 8 일 전 Rustにおける「検証するな、パースせよ」と型駆動設計 3 ポイント · 1件のコメント · 2026-02-23 C++を通じてRustの魅力を示したMatt Godboltの説得力 7 ポイント · 4件のコメント · 2025-05-07 Rustで「&中心の開発」を乗り越える 33 ポイント · 3件のコメント · 2023-03-13 Rustの核心 36 ポイント · 1件のコメント · 2025-08-23 1件のコメント GN⁺ 2024-05-17 Hacker News のコメント 良い記事。以前にプログラム検証をやった立場から見ると、Rust は形式手法を適用するのに最も有用な現代的言語のように見える Rust の規則は、形式化が難しいケースをかなり取り除いてくれる。残る大きな問題は、スレッドの観点と Rc/借用の観点から見たデッドロック解析で、この2つはある程度同等だ。Rust に静的デッドロック解析があれば、安全な逆参照ポインタも可能になりそうだし、すべての borrow/upgrade 呼び出しが失敗しないことを証明できれば、参照カウントの大半を取り除ける。そうなれば、可能な場合には内部可変性も無料で得られる 定理証明器の大きな問題は、定理を証明するのが好きな人たちが作っているため、形式主義に陥り、プログラマーや UI の感覚とずれてしまう点だ。証明義務の大半は SAT ソルバーで処理できるが、難しい問題にはより重いツールが必要になる。Coq は手作業が多すぎるし、投稿者は ACL2 が関数型に寄りすぎていると見ている。機械学習は定理証明器の方向づけには役立つかもしれない。証明そのものを任せるのは難しいが、制御フローとデータ利用がだいたい似ているコードから証明計画を推論することは可能に見える F* は、自動で証明してくれる神話のような言語に近い。SAT より強力な SMT ソルバーを使い、自動解決に失敗した場合は手動証明も可能 Firefox と Wireguard の暗号ルーチンは Rust ではなく F*、より正確には F* に組み込まれた低レベル DSL である Low* で書かれており、完全に検証されている https://project-everest.github.io/ https://mitls.org/ 同意するが、Lean は豊富なメタプログラミング機能のおかげで、対話型定理証明検証のユーザー体験が大きく進歩していると思う こうしたツールを Rust のような外部言語の検証に適用する際の問題は、証明が対象言語で書かれないため、開発者が2つの言語を学ばなければならない点だ。Creusot を書いた経験、Verus と Aeneas の作業、Why3 研究所での経験を踏まえて、「検証を意識した Rust」がどのような姿になるかを考えてきた。最初からそういう言語を作れば、Rust よりも検証のしやすさを段階的に高められるはずで、特に証明の難所で効果が大きいと思う Coq/Agda/Lean 系が証明分野の勝者になりそうだ。対話はフィードバックループとしてかなり良いモデルであり、すでに存在し、実際に動いているシステムでもある 組み込み機能として最も惜しいのは、「自分の証明に quickcheck を走らせてくれ」に相当する機能だ。コードがあり、真ではない性質を証明しようとして、なぜ証明できないのか頭を抱えることはよくある。証明の途中で意味のない状態に到達したら、「ここで反例を生成してみて」のようなコマンドが反例を出してくれるとよい。証明は経路依存性が大きく、一般に簡単ではないが、こうしたツールは偉大さにかなり近づいているように見える。コードを証明しようとする過程では、そのコードにバグがあり得る可能性も反映すべきだ 機械学習が定理証明器を導くというのは興味深い考えだ。機械学習システムが正しければ有効な証明へ導いて大きな利益があり、間違っていても大きな損失はない 証明器は誤った証明を導出するのではなく、単に有効な証明の導出に失敗するだけだ。このような性質を持つ機械学習の応用は多くないと思う 形式検証の専門家ではないが、伝統的な意味でのロックはあまり役に立たないと思う。どんなコンパイラもロックに関して有用なものを提供してくれず、単にリスクを受け入れて生きるしかない 実際、Rust におけるロックと参照カウントはランタイム上の構造物だ。Arc は Rust の RAII モデルを大きく壊しており、スコープが終わる前にデストラクタが実行されるべき scoped thread を取り除かざるを得なかった。グローバルな参照カウントには循環とリークの問題があり、再びグローバルな問題になる。完全になくすのは難しいだろうが、arena スタイルのスコープに閉じ込めるほうがよいと信じている。ロックにはチャネルのような非対称なデータ構造が必要に見える。Go ではチャネルを送信者と受信者に分け、送信 goroutine で defer close(ch) を設定でき、パニックが起きてもスレッドの残りが終われば実行が保証される。必ずしもチャネルである必要はないが、読み書き/生産者-消費者の役割を分離すれば、推論がはるかに容易になり、形式解析にも役立つと思う Hoare の1973年ごろの論文引用から始まって、もう2本目の記事まで続いているのが気に入っている。もともと boat の記事の HN スレッドに長いコメントを書き、その引用を Rust 中心の視点に傾けるのは boat の背景を考えれば理解できるが、Hoare の批判の範囲を人為的に狭めている、と書いた。 今では Grayson が、その狭い断片を出発点にして Rust のいくつかの興味深い領域と設計上の論点を論じている。今でも自分のコメントは正しいと思っているが、Grayson の記事から続いた議論は、出発点になった記事への技術的な不満を相殺するには十分だった。 1990年代半ばごろには、Hoare 自身も1970年代式の 健全性中心アプローチの基礎に何か誤りがあるかもしれないことに、すでに気づいていた: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h... その後、単純なテストより発展した非健全な手法が登場し、非健全な方法は健全な方法より先を行くようになったのだと思う。 前の記事を見逃した人には、このコメントのリンクが役に立つ: https://news.ycombinator.com/item?id=40355876 1973年は50年前であり、専門家の一生分に相当する。Hoare は本当にかなり近いところまで行っていた。 問題を見つけていたし、振り返れば、型システムで 共有 XOR 可変性を強制する解法は小さな一歩に見える。あのときその小さな一歩が解法だと分かっていれば、50年にわたる途方もない苦痛を減らせたはずだ。 boat による Hoare 論文引用について、もともと書いた考えはこうだ。Hoare の最初の引用と短い導入の後、筆者は「Tony Hoare が参照はジャンプに似ていると言ったときに扱っていたのは、可変でエイリアスを持つ状態の問題だった」と述べている。withoutboats は有名な Rust 開発者なので、こうした解釈は驚くものではない。 しかし引用文自体がその見方を補強しているようには見えない。Hoare がより一般的に、参照という意味論上の存在そのものを嘆いた内容を取り上げ、それを Rust の非エイリアス可変状態モデルに適用して問題を迂回しようとしている、と見ることはできる。ただしこれは、より大きな問題の狭い断片だけを直して、問題全体が消えたと言っているのに近い。抜け落ちている部分、とりわけ「Variables」節の冒頭と ALGOL 68 の例は、Hoare が単に可変状態ではなく、参照という意味論的概念そのものを批判していた、という方向にずっと強く傾いている。Rust が問題の一部を手なずけようとしていることは認めるが、どの言語もこの問題を「修正した」とは思わない。 この記事に対する称賛がなぜこれほど多いのか、よく分からない。プログラム解析の複数の分野を1段落で片づけてしまっている感じがする。Graydon は好きだし、その視点も尊重しているが、この段落は過度に単純化されている。 GC のある言語は強い局所推論の支援をあえて備えてこなかった、というような説明は藁人形論法だ。Pony のように型システムに領域を持たせながら GC も使う言語は存在した。また、ポインタ解析とエスケープ解析という分野全体があり、一意性を推論し、2つの参照がエイリアスになり得るかを判断する。静的型付けの核心も、クラスとフィールドという技術によってヒープを互いにエイリアスではない部分へ分割することにある。JavaScript の話ではないし、Java/C#/Scala や多数の GC 言語に可変状態についての局所推論がないかのように装ってはいけない。 一般の場合にこれを自動で完全に行うことはできず、実際には 分離論理にかなり近い何かが必要になる。Rust の借用検査の意味論も、単純化された分離論理の一種と見なせる。 クラスとフィールドは、可変状態について完全な局所推論を提供しない。クラス/オブジェクト A がクラス/オブジェクト B の可変状態に依存するようになり得るためだ。Java 式のクラス継承は、プログラムが時間とともに進化するにつれて、それ自体でさらに複雑さを増していく。 Graydon は、GC が強い局所推論を不可能にすると言ったわけではない。理由が何であれ、ほとんどの言語設計者がその目標に反する選択をしてきた、と言っているのであり、それは明らかに真に見える。 反例はもちろんあるが、Java、C#、Python のような主流の GC 付き汎用言語を見ると、その通りだ。オブジェクト指向の元々のアイデアは現在の アクターモデルに近く、所有されたデータ構造をメッセージ受け渡しだけで変更しようとしていた、という解釈は可能だ。しかし現実のオブジェクト指向実装は、その目標にほとんど近づいていない。Java は、同じオブジェクトへの可変参照を複数のオブジェクトに保存することを妨げない。この点はこの記事がよりうまく説明している: https://without.boats/blog/references-are-like-jumps/ 簡単なクイズとして、このコードは何を出力するだろうか? void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); } 追記: 二重否定を読み違えていた。読み直しても、やはりまだ混乱する。Java には JavaScript と違って局所推論がある、という意味なのだろうか? Graydon氏の文章は普段は好きだが、この記事は多くの形式手法に関する文章と同じく、その分野を知らない読者に誤解を与えかねない。鉛を金に変える方法が一桁程度改善したと言いながら、実用的な費用対効果に至るにはまだ29桁分ほど足りないとは言わないのに似ている。 エイリアスがないことが形式検証を大幅に容易にするかといえば、その通り。だからといって現実のプログラムを実用的かつ費用対効果の高い形で検証できるかといえば、まったくそうではない。日々形式検証されているプログラム、回路、コンポーネントは存在するが、それらは例外に近く、相対的に非常に小さく、特別に慎重な方法で作られている。局所的推論を助ける性質は重要だが、主流ソフトウェアの正しさを健全な方法で保証するやり方に実質的な変化をもたらすものではない。 ヒープもポインタも整数もなく、ブール変数だけがあり、ループも2回以上回れない、チューリング完全性からは程遠い言語のプログラムでさえ、TQBFに還元されるため実用的には検証できない。ある性質、たとえばメモリ安全性については可能でも、ソフトウェアが必要とするものには十分ではない。1970〜90年代には、最悪の場合の複雑性が扱いにくくても、言語の局所的な保証と構造が最悪ケースから逃れさせてくれるという期待があったが、その後そうではないことが証明された。人が実際に書くプログラムは最悪ケースから十分に離れていて、よいヒューリスティックが得られるという期待も、今では違うようだ。 関連内容を扱った発表がある: https://pron.github.io/posts/correctness-and-complexity 核心的な結果は、検証したい興味深い性質のほとんどは合成されないということだ。コンポーネント P1...Pn それぞれについて性質を証明しても、P1 ○ ... ○ Pn についてその性質を証明するコストは、nに対して超多項式的に増えるだけでなく、各コンポーネントのサイズに対しても超多項式的に増える。つまり分割しなかった場合と同じくらい難しく、正しさは分解できない。だから「かなり多くのものを検証できる」と「検証可能なものは大海の一滴でしかない」は同時に真であり、形式手法の議論ではこの隔たりがしばしば抜け落ちる。 この6年以上、HNで同じ論理を何百回も繰り返してきており、その間にもらった多くのコメントの後でも、ニュアンスはほとんど追加されていない。 完全に間違っているわけではないが、完全に正しいわけでもない。このテーマに関心のある多くの人々が、何百回もの反復の中でその点を示す機会を十分に持っていたにもかかわらず、立場がまったく進化していないのは驚きだ。こうした態度は病的な閉鎖性のように聞こえ、対話に参加する全員の時間を無駄にしてしまう。 健全性に焦点を当てることは、より正しいソフトウェアという目標に役立つというより、実際にはより成果を上げてきた手法から注意をそらしていると思う。理論的にも裏付けられた実用的手法があり、健全性こそが唯一の道だと考えていた人々を時に驚かせる: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h... こうしたことは繰り返し起きている。健全な方法に重要な改善が生まれている間にも、非健全な方法は実務において、より正しいソフトウェアへ向けてはるかに大きな前進を遂げている。ごく最近の例として https://antithesis.com がある。もちろん、特定の状況では健全な手法のほうが強力で実用的になり得るので、複雑なテーマではある。 小さなRustライブラリが unsafe を正しく使っているか検証できるようになる、と期待するのは合理的だ。それだけでも本当に有用だ。 F* の記事にも、いま関連するコメントを付けたところだ。構文だけを見れば主観的にはRustより F*/F# のほうが好みだが、開発中のショー制御ソフトウェアには Ada/SPARK2014 を使うことにした。 RustがAda/SPARK2014と同じような人々を引き寄せるには、C、Common Lisp、Prolog、Fortran、COBOLといった既存言語のように、公式に出版された標準が必要だ。AdaCoreとFerrous SystemsがAda/SPARK2014のようにRust向けの形式検証ツールを提供しようと協力しており、Rustも参入しつつあるが、まだ出版された標準はなく、AdaとSPARK2014の遺産は非常に大きい。 参照カウントは、厳密に非循環なデータに使うか、循環リークを許容できる場合に機能する、ある種の即時実行型の最適化されたGCと見なせる点が興味深い。Pythonは記事で説明されている参照カウント＋トレーシングの混合方式を使っており、トレーシング・コレクタをN個のリクエストごとに1回だけ走らせるよう強制している運用デプロイも見たことがある Perlは純粋な参照カウントだが弱参照があるため、循環構造のうちどの部分の参照を維持するかに注意を払う代わりに、参照カウントの観点ではデータを非循環にできる。Kokaは理論上は参照カウントを使うが、実際には可能な限りコンパイル時に持ち上げようとし、y = x + 1でxの参照が1つだけで、その後使われないことが保証されていれば、yに同じストレージを再利用してインプレース変更できる NimはORCを提供しており、これは自動参照カウントにBacon+RajanのRecyclerアルゴリズムの実装を加えたもの。このアルゴリズムは参照カウントベースのシステムで循環だけを回収するよう設計されていて、かなり速い。Rustの話に戻ると、stop-the-worldなRecycler実装がここにある: https://github.com/fitzgen/bacon-rajan-cc そしてこのフォークではbacon-rajan-cccクレートとして配布されている: https://github.com/mbartlett21/bacon-rajan-cc READMEのAlternative節には、同じ領域の別の実験へのリンクがある。Recycler論文が見つけにくければ、コピーをhttps://trout.me.uk/gc/以下にまとめておいたし、似た趣味ならhttps://trout.me.uk/lisp/以下の論文も楽しめるはず FirefoxもC++ DOMオブジェクトとJSを介した循環を管理するために、参照カウントとtrial deletionベースの循環コレクタを併用している。実際、Graydonが初期実装を担当した https://github.com/chc4/samsaraも見てみる価値がある。Rust向けに同じ並行GCアルゴリズムを実装している。C++実装はhttps://github.com/pebal/sgclにある プログラムの形式検証には性急さを感じる。プログラムが仕様を正しく実装しているという証明は、理論的には興味深いが実用上の有用性は小さい 正しい仕様を書くことは正しいプログラミングと同じくらい難しいので、難しい問題が解決されるのではなく移されるだけだ。形式手法には実用的な使いどころもあるが、出会うことはまれ 完全な仕様ならその通りだが、それが実際の目標ではない。普通、証明したいのはいくつかの中核的な性質だ。たとえば、この関数は必ず終了する、あの関数は必ずソート済み配列を返す、といったもの いったんそういうことができれば、前提条件として強制できる。たとえば、ある関数に配列を渡す前に、その配列があらかじめソート済みであることを示さなければならない、という具合だ 2024年5月15日に書かれ、その日はRust 1.0の9周年だった リンク先のBoatsの記事を読んだが素晴らしかった。Hoareの50年前の引用が今でも関連性を持ち、表現もとても良いことに驚いた もっと単純な形で、コンパイル時の型ガードのようなものを使えるとよい。trait boundが増殖すると、型レベルプログラムを読むのが難しくなる たとえばWhere <<::Output as G>::Output as H>::Output: HList + Zやtype Output = <<::Output as G>::Output as H>::Output;のような形だ。ここにCons>>>を入れ、TypeNumのU8のような数値も、それ自体がCons>>のネストなのだと気づく。この領域で進展を作り、望む検証をさせることはできるが、エラーメッセージが人間の開発者がコードを書くやり方と大きく異なるものになり得るし、実装も非常に苦痛だ 開発者体験が驚くべきものになる理由は、これが「ただの関数」ではなく、特定のジェネリクスと関連型の組み合わせだからだ。ランタイム風の検査を使いつつコンパイル時に実行したいが、そのためにはかなり違うコードを書く必要があった。結局、型レベルのコンパイル時Rustをより単純で関数型的かつ読みやすくすることが、こうした形式分析プロジェクトをメンテナーとユーザーにとって良い体験にする道かもしれない。要するにcomptime Rustが欲しい。そしてPin<&mut Self>ベースのFutureはすでに固まってしまったのかも気になる。async/awaitの別の内部実装を実験してみたいが、どこから始めればよいのか分からない
1件のコメント
Hacker News のコメント
良い記事。以前にプログラム検証をやった立場から見ると、Rust は形式手法を適用するのに最も有用な現代的言語のように見える
Rust の規則は、形式化が難しいケースをかなり取り除いてくれる。残る大きな問題は、スレッドの観点と
Rc/借用の観点から見たデッドロック解析で、この2つはある程度同等だ。Rust に静的デッドロック解析があれば、安全な逆参照ポインタも可能になりそうだし、すべての borrow/upgrade 呼び出しが失敗しないことを証明できれば、参照カウントの大半を取り除ける。そうなれば、可能な場合には内部可変性も無料で得られる定理証明器の大きな問題は、定理を証明するのが好きな人たちが作っているため、形式主義に陥り、プログラマーや UI の感覚とずれてしまう点だ。証明義務の大半は SAT ソルバーで処理できるが、難しい問題にはより重いツールが必要になる。Coq は手作業が多すぎるし、投稿者は ACL2 が関数型に寄りすぎていると見ている。機械学習は定理証明器の方向づけには役立つかもしれない。証明そのものを任せるのは難しいが、制御フローとデータ利用がだいたい似ているコードから証明計画を推論することは可能に見える
Firefox と Wireguard の暗号ルーチンは Rust ではなく F*、より正確には F* に組み込まれた低レベル DSL である Low* で書かれており、完全に検証されている
https://project-everest.github.io/
https://mitls.org/
こうしたツールを Rust のような外部言語の検証に適用する際の問題は、証明が対象言語で書かれないため、開発者が2つの言語を学ばなければならない点だ。Creusot を書いた経験、Verus と Aeneas の作業、Why3 研究所での経験を踏まえて、「検証を意識した Rust」がどのような姿になるかを考えてきた。最初からそういう言語を作れば、Rust よりも検証のしやすさを段階的に高められるはずで、特に証明の難所で効果が大きいと思う
組み込み機能として最も惜しいのは、「自分の証明に quickcheck を走らせてくれ」に相当する機能だ。コードがあり、真ではない性質を証明しようとして、なぜ証明できないのか頭を抱えることはよくある。証明の途中で意味のない状態に到達したら、「ここで反例を生成してみて」のようなコマンドが反例を出してくれるとよい。証明は経路依存性が大きく、一般に簡単ではないが、こうしたツールは偉大さにかなり近づいているように見える。コードを証明しようとする過程では、そのコードにバグがあり得る可能性も反映すべきだ
証明器は誤った証明を導出するのではなく、単に有効な証明の導出に失敗するだけだ。このような性質を持つ機械学習の応用は多くないと思う
実際、Rust におけるロックと参照カウントはランタイム上の構造物だ。
Arcは Rust の RAII モデルを大きく壊しており、スコープが終わる前にデストラクタが実行されるべき scoped thread を取り除かざるを得なかった。グローバルな参照カウントには循環とリークの問題があり、再びグローバルな問題になる。完全になくすのは難しいだろうが、arena スタイルのスコープに閉じ込めるほうがよいと信じている。ロックにはチャネルのような非対称なデータ構造が必要に見える。Go ではチャネルを送信者と受信者に分け、送信 goroutine でdefer close(ch)を設定でき、パニックが起きてもスレッドの残りが終われば実行が保証される。必ずしもチャネルである必要はないが、読み書き/生産者-消費者の役割を分離すれば、推論がはるかに容易になり、形式解析にも役立つと思うHoare の1973年ごろの論文引用から始まって、もう2本目の記事まで続いているのが気に入っている。もともと boat の記事の HN スレッドに長いコメントを書き、その引用を Rust 中心の視点に傾けるのは boat の背景を考えれば理解できるが、Hoare の批判の範囲を人為的に狭めている、と書いた。
今では Grayson が、その狭い断片を出発点にして Rust のいくつかの興味深い領域と設計上の論点を論じている。今でも自分のコメントは正しいと思っているが、Grayson の記事から続いた議論は、出発点になった記事への技術的な不満を相殺するには十分だった。
その後、単純なテストより発展した非健全な手法が登場し、非健全な方法は健全な方法より先を行くようになったのだと思う。
問題を見つけていたし、振り返れば、型システムで 共有 XOR 可変性を強制する解法は小さな一歩に見える。あのときその小さな一歩が解法だと分かっていれば、50年にわたる途方もない苦痛を減らせたはずだ。
しかし引用文自体がその見方を補強しているようには見えない。Hoare がより一般的に、参照という意味論上の存在そのものを嘆いた内容を取り上げ、それを Rust の非エイリアス可変状態モデルに適用して問題を迂回しようとしている、と見ることはできる。ただしこれは、より大きな問題の狭い断片だけを直して、問題全体が消えたと言っているのに近い。抜け落ちている部分、とりわけ「Variables」節の冒頭と ALGOL 68 の例は、Hoare が単に可変状態ではなく、参照という意味論的概念そのものを批判していた、という方向にずっと強く傾いている。Rust が問題の一部を手なずけようとしていることは認めるが、どの言語もこの問題を「修正した」とは思わない。
この記事に対する称賛がなぜこれほど多いのか、よく分からない。プログラム解析の複数の分野を1段落で片づけてしまっている感じがする。Graydon は好きだし、その視点も尊重しているが、この段落は過度に単純化されている。
GC のある言語は強い局所推論の支援をあえて備えてこなかった、というような説明は藁人形論法だ。Pony のように型システムに領域を持たせながら GC も使う言語は存在した。また、ポインタ解析とエスケープ解析という分野全体があり、一意性を推論し、2つの参照がエイリアスになり得るかを判断する。静的型付けの核心も、クラスとフィールドという技術によってヒープを互いにエイリアスではない部分へ分割することにある。JavaScript の話ではないし、Java/C#/Scala や多数の GC 言語に可変状態についての局所推論がないかのように装ってはいけない。
クラスとフィールドは、可変状態について完全な局所推論を提供しない。クラス/オブジェクト A がクラス/オブジェクト B の可変状態に依存するようになり得るためだ。Java 式のクラス継承は、プログラムが時間とともに進化するにつれて、それ自体でさらに複雑さを増していく。
反例はもちろんあるが、Java、C#、Python のような主流の GC 付き汎用言語を見ると、その通りだ。オブジェクト指向の元々のアイデアは現在の アクターモデルに近く、所有されたデータ構造をメッセージ受け渡しだけで変更しようとしていた、という解釈は可能だ。しかし現実のオブジェクト指向実装は、その目標にほとんど近づいていない。Java は、同じオブジェクトへの可変参照を複数のオブジェクトに保存することを妨げない。この点はこの記事がよりうまく説明している: https://without.boats/blog/references-are-like-jumps/
void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }追記: 二重否定を読み違えていた。読み直しても、やはりまだ混乱する。Java には JavaScript と違って局所推論がある、という意味なのだろうか?
Graydon氏の文章は普段は好きだが、この記事は多くの形式手法に関する文章と同じく、その分野を知らない読者に誤解を与えかねない。鉛を金に変える方法が一桁程度改善したと言いながら、実用的な費用対効果に至るにはまだ29桁分ほど足りないとは言わないのに似ている。
エイリアスがないことが形式検証を大幅に容易にするかといえば、その通り。だからといって現実のプログラムを実用的かつ費用対効果の高い形で検証できるかといえば、まったくそうではない。日々形式検証されているプログラム、回路、コンポーネントは存在するが、それらは例外に近く、相対的に非常に小さく、特別に慎重な方法で作られている。局所的推論を助ける性質は重要だが、主流ソフトウェアの正しさを健全な方法で保証するやり方に実質的な変化をもたらすものではない。
ヒープもポインタも整数もなく、ブール変数だけがあり、ループも2回以上回れない、チューリング完全性からは程遠い言語のプログラムでさえ、TQBFに還元されるため実用的には検証できない。ある性質、たとえばメモリ安全性については可能でも、ソフトウェアが必要とするものには十分ではない。1970〜90年代には、最悪の場合の複雑性が扱いにくくても、言語の局所的な保証と構造が最悪ケースから逃れさせてくれるという期待があったが、その後そうではないことが証明された。人が実際に書くプログラムは最悪ケースから十分に離れていて、よいヒューリスティックが得られるという期待も、今では違うようだ。
関連内容を扱った発表がある: https://pron.github.io/posts/correctness-and-complexity
核心的な結果は、検証したい興味深い性質のほとんどは合成されないということだ。コンポーネント P1...Pn それぞれについて性質を証明しても、P1 ○ ... ○ Pn についてその性質を証明するコストは、nに対して超多項式的に増えるだけでなく、各コンポーネントのサイズに対しても超多項式的に増える。つまり分割しなかった場合と同じくらい難しく、正しさは分解できない。だから「かなり多くのものを検証できる」と「検証可能なものは大海の一滴でしかない」は同時に真であり、形式手法の議論ではこの隔たりがしばしば抜け落ちる。
完全に間違っているわけではないが、完全に正しいわけでもない。このテーマに関心のある多くの人々が、何百回もの反復の中でその点を示す機会を十分に持っていたにもかかわらず、立場がまったく進化していないのは驚きだ。こうした態度は病的な閉鎖性のように聞こえ、対話に参加する全員の時間を無駄にしてしまう。
こうしたことは繰り返し起きている。健全な方法に重要な改善が生まれている間にも、非健全な方法は実務において、より正しいソフトウェアへ向けてはるかに大きな前進を遂げている。ごく最近の例として https://antithesis.com がある。もちろん、特定の状況では健全な手法のほうが強力で実用的になり得るので、複雑なテーマではある。
unsafeを正しく使っているか検証できるようになる、と期待するのは合理的だ。それだけでも本当に有用だ。F* の記事にも、いま関連するコメントを付けたところだ。構文だけを見れば主観的にはRustより F*/F# のほうが好みだが、開発中のショー制御ソフトウェアには Ada/SPARK2014 を使うことにした。
RustがAda/SPARK2014と同じような人々を引き寄せるには、C、Common Lisp、Prolog、Fortran、COBOLといった既存言語のように、公式に出版された標準が必要だ。AdaCoreとFerrous SystemsがAda/SPARK2014のようにRust向けの形式検証ツールを提供しようと協力しており、Rustも参入しつつあるが、まだ出版された標準はなく、AdaとSPARK2014の遺産は非常に大きい。
参照カウントは、厳密に非循環なデータに使うか、循環リークを許容できる場合に機能する、ある種の即時実行型の最適化されたGCと見なせる点が興味深い。Pythonは記事で説明されている参照カウント＋トレーシングの混合方式を使っており、トレーシング・コレクタをN個のリクエストごとに1回だけ走らせるよう強制している運用デプロイも見たことがある
Perlは純粋な参照カウントだが弱参照があるため、循環構造のうちどの部分の参照を維持するかに注意を払う代わりに、参照カウントの観点ではデータを非循環にできる。Kokaは理論上は参照カウントを使うが、実際には可能な限りコンパイル時に持ち上げようとし、
y = x + 1でxの参照が1つだけで、その後使われないことが保証されていれば、yに同じストレージを再利用してインプレース変更できるNimはORCを提供しており、これは自動参照カウントにBacon+RajanのRecyclerアルゴリズムの実装を加えたもの。このアルゴリズムは参照カウントベースのシステムで循環だけを回収するよう設計されていて、かなり速い。Rustの話に戻ると、stop-the-worldなRecycler実装がここにある: https://github.com/fitzgen/bacon-rajan-cc そしてこのフォークではbacon-rajan-cccクレートとして配布されている: https://github.com/mbartlett21/bacon-rajan-cc READMEのAlternative節には、同じ領域の別の実験へのリンクがある。Recycler論文が見つけにくければ、コピーをhttps://trout.me.uk/gc/以下にまとめておいたし、似た趣味ならhttps://trout.me.uk/lisp/以下の論文も楽しめるはず
プログラムの形式検証には性急さを感じる。プログラムが仕様を正しく実装しているという証明は、理論的には興味深いが実用上の有用性は小さい
正しい仕様を書くことは正しいプログラミングと同じくらい難しいので、難しい問題が解決されるのではなく移されるだけだ。形式手法には実用的な使いどころもあるが、出会うことはまれ
いったんそういうことができれば、前提条件として強制できる。たとえば、ある関数に配列を渡す前に、その配列があらかじめソート済みであることを示さなければならない、という具合だ
2024年5月15日に書かれ、その日はRust 1.0の9周年だった
リンク先のBoatsの記事を読んだが素晴らしかった。Hoareの50年前の引用が今でも関連性を持ち、表現もとても良いことに驚いた
もっと単純な形で、コンパイル時の型ガードのようなものを使えるとよい。trait boundが増殖すると、型レベルプログラムを読むのが難しくなる
たとえば
Where <<::Output as G>::Output as H>::Output: HList + Zやtype Output = <<::Output as G>::Output as H>::Output;のような形だ。ここにCons>>>を入れ、TypeNumのU8のような数値も、それ自体がCons>>のネストなのだと気づく。この領域で進展を作り、望む検証をさせることはできるが、エラーメッセージが人間の開発者がコードを書くやり方と大きく異なるものになり得るし、実装も非常に苦痛だ開発者体験が驚くべきものになる理由は、これが「ただの関数」ではなく、特定のジェネリクスと関連型の組み合わせだからだ。ランタイム風の検査を使いつつコンパイル時に実行したいが、そのためにはかなり違うコードを書く必要があった。結局、型レベルのコンパイル時Rustをより単純で関数型的かつ読みやすくすることが、こうした形式分析プロジェクトをメンテナーとユーザーにとって良い体験にする道かもしれない。要するに
comptimeRustが欲しい。そしてPin<&mut Self>ベースのFutureはすでに固まってしまったのかも気になる。async/awaitの別の内部実装を実験してみたいが、どこから始めればよいのか分からない