route127の日記： 片付けできなかったよ言語

12月初旬にnull安全が流行してたような感じがしたがその関連記事読んでてコンパイラが未定義動作を最適化に用いる話をしていた。
普段perlしか使わないので最近のC言語とかコンパイラの最適化とかよくわかりはしないのだが以前x86でのud2命令の話(2009)を読んだこともあったので、そういうものなのか程度に思っていた。
（null参照については2009年にストーリーにもなっていたようだ。）

それとは別に数セミの記事(2015)でガリグ(Jacques Garrigue)が証明支援系Coqについて書いた記事の中に出てくるCompCertが気になっていた。
実際にエアバスで使われてるCコンパイラ、ということであったが今回色々調べていく中でXavierスライドなんかを見てると、そもそも欧州航空業界のモデルベース開発なんかでSimulinkなんかから生成されたCソースを最適化を掛けながらコンパイルしつつ実行時エラーもなくしたいみたいな需要があってのことらしい。
大体CompCertに4人年（48人月）かかってるそうだ。
モデルベース開発と言うと直近の機械学会誌がモデルベースシステムズエンジニアリング関連だった。
システムズエンジニアリング寄りの記事だったがフランス産業界の話なんかも掲載されていた。
CompCert（Cコンパイラ）もだがScicos（制御系設計）とかFreeFEM++（有限要素法解析）とかにもINRIAは関わっていてフランスすごいなと思う。
後述するAdaも元々フランス人の手によるものだと最近知った。

フランス産業界がそうこうする中、アメリカはどうしていたかと言えば、F-35戦闘機開発に当たってソフトウェア開発にAdaを採用することは、英国側の懸念や動員できるプログラマの数等の問題もあり、コーディング規約JSF++を制定した上でC++を採用したらしい。
MISRA-C++のスライドにはF-35のプログラム開発には4万人のプログラマが動員されたとある。
モデル駆動開発(MDD)としてUMLからのコード生成なんかもしていたようなのでフランスとも状況は似てはいる。
ただ生成されたコードを検証済みコンパイラにかけるか、規約に基づくコードを出力させるというアプローチという違いはあるようだ。
JSF++は自動車業界などで用いられるsafer-Cの実装としてのMISRA-Cなんかも関わりは深いらしい。
simulinkでもMISRA-C:2004準拠コードの出力が出来るそうだ。
結局のところメモリ保護の十分でない弱い型付け言語であるCを強い型付け言語であるAda並みの型安全を実現するためにあれこれ苦労してるということなのか。

日本でもメモリ安全なコードを生成するANSI標準準拠コンパイラを開発しているらしい。
文部科学省の資料にはメモリ安全C言語コンパイラ(FSC)、情報漏洩防止C言語コンパイラ(VITC) 、OS用型付きアセンブリ(TALK)なんかも載っている。
実際FSCはOpenSSLやBIND9で有用性の検証を行っているそうだ。

#弱い片付け人間なので部屋は片付きませんでした。