形式化願望の願望

http://www.radiumsoftware.com/0607.html#060720

Standard MLは（Schemeも？）、形式的定義のある数少ない実用的言語の一つかと。定理証明器で検証できるJava（＆Javaバイトコード）のサブセットもどんどん大きくなっているので、もう数十年〜数百年ぐらいすれば、形式的仕様と現実的実装が一致するようになるのではないでしょうか、と希望的観測。もっとも、たとえフルセットを検証しなくても、Javaのinner classみたいに（極めて小さい）サブセットをformalizeする途中の過程で、いろいろな実装のバグが発見されたりしていますが。