ハクソク

世界を動かす技術を、日本語で。

完璧に近づけるプログラミング言語

27日前原文(alok.github.io)

概要

  • 40種類以上のプログラミング言語を列挙し、Bay Area特有の会話を紹介
  • Leanが「perfectable（完璧化可能）」な言語である理由を解説
  • 型システム・定理証明・メタプログラミングの重要性をLeanを例に説明
  • Leanによるカスタム構文とAPI設計の柔軟性をデモ
  • Leanのコミュニティと他の定理証明系言語との違いを強調

40種類のプログラミング言語とBay Area文化

  • Sydney Von Arxとのパーティで「40個のプログラミング言語を挙げられるか？」という質問
  • Bay Areaらしい会話の一例
  • Racket、Agda、Clean、Elm、TypeScript、sh、ASP、Verilog、JavaScript、Scheme、Rust、Nim、INTERCAL、sed、Isabelle、Visual Basic、zsh、Alokscript、Coq、Idris、Hack、Prolog、Whitespace、PureScript、Go、Odin、Haskell、Python、tcsh、Unison、Clingo、bash、Java、Zig、Cyclone、PHP、awk、C、ActionScript、C++の列挙
  • どの言語にも特徴と進化傾向が存在

Leanが「perfectable」な理由

  • Lean は「完璧」ではないが「完璧化可能（perfectable）」な言語
  • Lean自身でLeanの性質や事実を記述・証明可能
  • コードに関する性質を言語自身で活用できる設計
  • 例：常に5を返す関数returnFiveの証明
    • TypeScriptや他の多くの言語では型や性質の活用に制約
    • Leanでは定理として記述・証明が容易

型システムの進化と定理証明

  • 型がない言語も、後に型アノテーションや型システムを導入する傾向
    • 例：PHP 7.4、Pythonの型アノテーション、TypeScript、Rust
  • 型システムの拡張・活用がプログラミング言語の進化の本質
  • C++テンプレートやRustのconstificationなど、コンパイル時計算の重視
  • 最も正しい方法は「依存型（dependent types）」の導入
    • 依存型は定理証明の基盤
    • 型の上で型の等価性を証明するインフラが必要＝定理証明器
  • 依存型言語は定理証明器に成長可能
    • そのためには「theorem proving infrastructure（定理証明インフラ）」の整備が不可欠

Leanのメタプログラミングとカスタム構文

  • メタプログラミングやカスタム構文の柔軟性がLeanの大きな特徴
    • 多くの言語はメタプログラミングが不便（Rustのプロシージャルマクロ等）
    • Leanはシームレスに実現可能
  • Tic-tac-toe（○×ゲーム）のカスタム構文例
    • 独自の構文カテゴリtttCell, tttRow, tttBoardSyntaxの宣言
    • board!構文による視覚的なボード表現
    • 構文の解釈を容易に差し替え可能
  • 型システムとメタプログラミングの連携
    • API設計の階層化とカプセル化が容易
    • 将来的には「メタメタプログラミング」も期待

Leanの定理証明とパフォーマンス

  • 定理証明能力が言語進化の「収束的進化」の結果
  • パフォーマンスの重要性
    • LeanはまだRustほど高速ではないが、最適化の余地が大きい
    • 証明によるコード等価性で最適化が容易
  • 例：returnFive a + 1 = 6の証明
    • 証明済みならコンパイラが自由に置換可能
  • 開発者（Leo de Moura）も後方互換性より進化を重視
  • AI時代にはコードの書き換えが容易
    • 定理証明器は究極のリファクタリングツール

Leanコミュニティと他言語との比較

  • Leanは同種の言語の中で唯一成長中
  • Coq、Idris、Agdaは競争力減少
    • Idris、F*はコミュニティ規模でLeanに及ばず
  • Leanは定理証明と実用的なプログラミング能力の両立
  • 実際にLeanコミュニティが活発に拡大中

コーディングの原点

  • Eliza Zhangとの賭けがきっかけでC言語に挑戦
  • 「できない」という言葉への反発がコーディング開始の動機
  • 初心を忘れず、挑戦し続ける姿勢の重要性

Hackerたちの意見

これが僕がLeanに興味を持つきっかけになったログ投稿なんだけど、まだ触ってないんだよね。https://kirancodes.me/posts/log-ocaml-to-lean.html

└

いい投稿ですね。ありがとう！

Fortran、Basic、APL、Beta、Odin、Self、C、C++、Objective-C、C#、C--、D、Scheme、Clojure、F-Script、Eiffel、COBOL、Ocaml、Haskell、Snobol、Crystal、Forth、Python、Lisp、Brainfuck、Java、Oak、Javascript、TypeScript、Wasm、Logo、Elang、Elixir、Gleam、Elm、Zig、m4、Tcl、Simula、Smalltalk。面白い挑戦だね。著者とは違って、特に付け加えることはないけど、「私はこれを...で書いたわけじゃない」と言いたかっただけ。

└

確かに！A-B-Cで20くらいまで行ったけど、その後はなんか難しくなった。C系の言語がたくさんあるのは分かるけど、A*系の言語がこんなにあるとは思わなかった（apl、ada、agda、alice、algol、applescript、apex、ampl、assembly…）。

└

C--！それを忘れてた。最初のGlasgow Haskell CompilerのILRだね。

Lean4大好き！クラス最高の関数型プログラミング言語だと思う。でも、標準ライブラリに非構成的公理を組み込むことで「完璧性」がちょっと制約されてる気がする。カーネルはこれを減らせない不透明な定数として扱わなきゃいけないからね。数学的なプログラミングにはAgdaを使うことが多いけど、将来的にはLean4がHaskellの代わりになってほしいな。

└

個人的には、F*はproof-orientedプログラミングにはLean4よりずっと良い選択だと思う。後者はまだ数学に関することが多いけど、前者にはこんなのがあるしね。https://fstarlang.github.io/lowstar/html/LowStar.html

残念ながら、Leanの配布サイズはLean 3の頃の約15 MiBから、今では解凍すると2.5 GiB以上になってて、理由が全くわからない。これは多すぎるよ。v4.0.0-m1でも90 MBのアーカイブだったし。Leanの作者たちはもうこのことを気にしてないみたい。Lean 3はLean、Coq、Agdaの中で一番軽量な定理証明器だったのに、Lean 4はこのビッグスリーの中で一番重いんだ。すごく悲しい。個人的には、最後のアップデートで統一が変な感じで壊れたから、Leanの使用をやめたよ。

└

Leanは一番重いわけじゃないよ。Isabelleがその座を取る可能性が高いね。メインアーカイブにはVSCodiumが含まれているから。

└

静的リンクの驚き？元々LeanはC++で書かれていて、動的にリンクされた実行可能ファイルだったと思う。

└

それに、デフォルトのパッケージレジストリにGithubを使ってるのがあんまり好きじゃない。でも、この言語がMicrosoft内で作られたから、仕方ないのかな。

└

名前が今は皮肉に聞こえるね。

彼らは実際にビジネスを展開しているプロジェクトなの？大学ではCoqを触ったことがあるけど、F#が保険会社で使われているのを見たことがある。LeanについてはHNの投稿で初めて聞いたよ。

└

実行すること自体はわからないけど、実際のアプリケーション（製品やサービスのために作られたもの）は存在するよ。IsabelleやLeanの著名な実践者はAWSだね。もっと実用的なツールとしてTLA+もある。これらの証明補助ツールの中で最も広く使われているのは、形式的に検証されたコンパイラ、例えばcompcertで、航空業界などの厳しく規制された業界で使われていることが多いよ。[0]: https://isabelle.systems/zulip-archive/stream/247541-Mirror.... と https://lean-lang.org/ (Cedar)

Leanでコンピュータ代数の簡約器をいじってるんだ：https://github.com/dharmatech/symbolism.lean。Leanは驚くほど表現力があるよ。

完璧にできるから。完璧ではないけど、完璧にできる。Leanについての特性をLeanで書けるんだ。ホモアイコニシティって知ってる？Lispは最も古い高級プログラミング言語の一つで、今でも使われてるよ。

└

じゃあ、彼らが「Lispの呪い」をどう避けるつもりなのかが問題だね（私の言葉で言うと、言語があまりにも力を与えると変なことをするようになって、ちょっと強力すぎるものを使いたがる人を引き寄せて、生産性のない文化になっちゃう）。

└

サイトが見れない（組織が理由でGithubをブロックしてる）けど、もしForthがそんなにスタックに偏ってなかったら、これもForthに似てるんじゃないかな。

└

ホモアイコニシティって知ってる？興味がある人のためにここに置いとくね、関連性ありそうだし: https://github.com/replikativ/ansatz Ansatzは、帰納的構成法（CIC）に基づいたClojure用の検証済みプログラミングライブラリだよ。Lean 4を支えるのと同じタイプ理論だね。

└

ここに来た理由は「もうLispがあるから」ってコメントしたかったから。

└

うーん。ホモアイコニシティってあんまり明確な定義がないんだよね（例えば、Shriram Krishnamurthiの考えを見てみて [0][1]）。でも、その事実を軽く流しても、これは文法的な特性で、引用された文は意味論についてのことだから。言語をLisp（またはその子孫の一つ）に変えても、意味的には何も得られないよ。[0] ShriramはRacketプロジェクトの初期メンバーだから、少なくとも30年間はLispに似た領域で働いてきたし、特に文法に関する問題に焦点を当てたLispの派生系で活動してるんだ。だから、このトピックに関しては彼を引用するのは妥当だと思うよ。[1] https://parentheticallyspeaking.org/articles/bicameral-not-h...

何でもやるのが一番簡単なのは、ちゃんとやることだ。もしこれが本当なら、どんなに素晴らしい世界になるだろうね！

パーティーで、Sydney Von Arxが40のプログラミング言語を挙げられるか聞いてきた。試しに（見ずに）やってみたよ。JavaScript、QBasic、PHP、Haskell、C、C++、Ada、Algol、Racket、Scheme、Clojure、Common-Lisp、GOOL、Fortran、Awk、Postscript、Forth、C#、F#、Lua、Java、D、Odin、Rust、Zig、Julia、Python、Nim、MATLAB、Bash、Brainfuck、Arnold-C、Intercal、Gleam、Unison、Ruby、Crystal、Erlang、Go、TCL、ふぅ！

└

楽しい挑戦だね！私のリストは、Ada、Agda、Assembly、Awk、BASIC、Brainfuck、C、C#、C++、COBOL、Curry、D、Elixir、Elm、F#、FORTRAN、Gleam、GLSL、Go、Haskell、HCL、Idris、Intercal、Java、Javascript、Objective-C、Ocaml、Pascal、Pony、Prolog、Python、R、Ruby、Rust、Sh、Sketch、Swift、Typescript、Visual Basic、Zigだよ。

普段は権威に頼るのは好きじゃないけど、今回はちょっと「完璧」すぎる。「言語には二種類しかない。文句を言われるものと、誰も使わないものだ。」- ビャーネ・ストロストルップ