fixedpoint.jp - Should Your Specification Language Be Typed?

Should Your Specification Language Be Typed?

今年最後に読んだ論文は "Should Your Specification Language Be Typed?" になりました。

著者のうち Leslie Lamport の方が、公理論的集合論を基礎に置いた untyped な specification language が

• より柔軟で
• 何でも表現できる

という利点を持つという議論を中心に行っています。一方で、もう1人の著者 Lawrence C. Paulson が typed な言語が

• ある種の仕様を記述するのが簡単になる
• 必要ならば(predicate) subtyping や overloading、datatype で表現できる範囲が増す
• mechanical な支援で人間が介在しなくてもある種のエラーを検出できる

という利点を持つということを述べています。このように対照的な見解をもつ2人が議論を共有して共通の認識に達したまとめが参考になります。

「typed な specification language が untyped なものよりもいいのかどうか」というテーマは結論に至るのが難しいですが、はっきりと述べられている次の点に注目しました:

• programming language の型についての議論と specification language の型についての議論をはっきり区別する
• typed/untyped のいずれが自然かという哲学的な議論はせず、実用的な視点から議論する
• untyped な言語で、型情報を annotation で付加するのはどう?という提案 ... ずるい