2026 年に読む “The Definition of Standard ML” 〜 現代の堅牢なソフトウェア設計の源流として
処理系が事実上の仕様: Python, Ruby, Rust
自然言語の仕様書: JavaScript, Java, C
SML は形式的な推論規則
どちらかというと自然言語の仕様書に近い
自然意味論で記述（形式的に導出される）
プログラミング言語そのものを扱う人を想定し、文法だけじゃなくて形式的な意味を記述した
どう実装すべきかではなく、どう振る舞うべきか
仕様はあるが、実装は自由
型推論（Algorithm W, J）・構文解析アルゴリズム、メモリ管理（ヒープ, スタック, GC）などは含まれていない
「形式的な仕様が何を定めたか / 定めなかったか」を見ていく
意味論の分離
静的意味論: プログラムの正当性を判定
動的意味論: プログラムの計算結果を定義
e.g. let 式と関数適用を 推論規則 による例 値の計算に型は不要
∵ 関数適用の推論規則に、関数でない値が適用されないケースはない
型検査が通れば、実行時の評価は破綻しないことを書ける
型の抽象化
TypeScript ではレビュー、Lint、慣習でカバーする必要がある（Branded types）
公称型があれば十分？: No
SML では型を隠蔽できる（不透明シグネチャ: opaque signature）
互換性に価値がある場合は、透明シグネチャを使う場合もある（選択できる）
OCaml は不透明のみ
structure（実装）
signature（インタフェース）
structure $ :> signature
type t と書くと t = string だった事実が型環境から消える
e.g. 推論規則と それに UserId を当てはめてみる
型の依存関係
DI は起動時に、遅延注入なら実行時にエラー（落ちる）
SML には Functor というのがある
structure を受け取って、新しい structure を返す
静的意味論: Functor を満たすか検証 + 型名の生成
動的意味論: モジュール本体のコードを実行、型の解決は行わない
実行時にシグネチャが合わなかったというのが存在しない
可変状態の対象
SML は非純粋で可変セル（ref）が作成できる
多相性（Generics）と可変状態を組み合わせると、型安全を壊しかねない
Haskell: IO の中に閉じ込める
Rust: let 束縛は多相化 NG
SML: 値である式だけ多相化 OK
ref [], compose (id, id)]
本当に安全かではなく、構文的にチェック
η 変換すれば回避できる: fn でラップする
実際に計測した上で規則の単純さと描きやすさを重視
コンパイラへの信頼
厳密さに差はあっても、検証や議論の下地はある
CakeML
コンパイラの各パスが意味を保存することを証明した処理系
保存の定理を合成するとこのコンパイラは正しいまでが証明する
LLM
生成されたコード自体には機械的にチェックがかけられる
しかし、自然言語の要求と実装の関係は機械的にチェックできない
そのため、要求を検査できる形に書き下ろす必要がある
The Defitnion と同じように、機械がチェックできる不変条件でガードできるよう整備すべき
The Definition は 97' のあと改定されていない（議論はあったが体制は残らず）
後継としては、WASM？
推論規則が W3C 仕様が本文
健全性は機械検証
W3C が改定を継続