今年最後に読んだ論文は "Should Your Specification Language Be Typed?" になりました。
著者のうち Leslie Lamport の方が、公理論的集合論を基礎に置いた untyped な specification language が
という利点を持つという議論を中心に行っています。一方で、もう1人の著者 Lawrence C. Paulson が typed な言語が
という利点を持つということを述べています。このように対照的な見解をもつ2人が議論を共有して共通の認識に達したまとめが参考になります。
「typed な specification language が untyped なものよりもいいのかどうか」というテーマは結論に至るのが難しいですが、はっきりと述べられている次の点に注目しました: