Salt v1.0.0 – Z3定理証明機能をコンパイラ内に持つシステム言語

- Saltは、コンパイラ内部にZ3定理証明器を統合した新しいシステムプログラミング言語。v1.0.0に達したことで、実用的な開発が可能な段階に入ったことを示す。 - Z3はMicrosoft Researchが開発したSAT/SMTソルバーで、制約充足問題や論理式の充足可能性を判定できる。これにより、コンパイル時にメモリ安全性や並行処理の正当性を数学的に検証できる。 - 従来のシステム言語（C, Rust, Zigなど）は型システムや所有権モデルで安全性を保証するが、Saltは定理証明を直接コンパイラに組み込むことで、より強力な静的検証を目指す。 - システムプログラミング言語の分野では、検証機能の強化が近年のトレンド。Rustの「怖くない並行性」や、検証付き言語Dafny・F*などが先行例として存在する。