関数型言語マニアのための論文紹介４：安全なC言語処理系

CCured: Type-Safe Retrofitting of Legacy Software. George C. Necula, Jeremy Condit, Matthew Harren, Scott McPeak, and Westley Weimer. TOPLAS 27(3), May 2005.

http://manju.cs.berkeley.edu/ccured/toplas.pdf

マニュアルとダウンロードはこちら↓

http://manju.cs.berkeley.edu/ccured/

「どこが関数型言語やねん！」と思った方は続きをお読みください。

「関数型言語は安全」「C言語は安全じゃない」とよく言われますが、特定の実装ではなく言語の仕様をよーーーく読むと、（ある厳密な意味において）「安全」なC言語の実装もほぼ可能であることがわかります。これにより、スタックオーバーフローなど特定の場合だけでなく、ほぼ「すべて」の「安全」でないバグを実行時検出できます。しかも、実行時検査のオーバーヘッドは数％〜２倍ぐらいで済みます。これらを実現するために、関数型言語やらλ計算やら型理論やらで培養された理論や技術が応用されまくっています。っていうか実装がOCamlだし。

なお、同様のアイディアは日本で↓先行して研究されています。:-)

http://web.yl.is.s.u-tokyo.ac.jp/~oiwa/ja_JP.ISO-2022-JP/FailSafe-C.html

この「Fail-Safe C」については、すでに研究レベルの実装はありますが、公開されていないはずです（検索でヒットするのは別の方による実装）。実用レベルの実装は産総研で開発が進行中のはずです（と身内の宣伝）。

余談：プログラミング言語が「安全」(safe)ないし「型安全」(type-safe）という言葉は定義が難しくて、

http://d.hatena.ne.jp/sumii/20051107/1131321743

でも書いたように研究者間でも意見が一致していません。「Fail-Safe CやCCuredが（実装として）安全」というのは、その中の一つの定義によります。大ざっぱにいうと「Schemeが（言語として）安全」という場合の意味に近いです。