ソフトウェアにバグがあるのは仕方のないことなのか？ | TechCrunch Japan
http://jp.techcrunch.com/2016/10/03/20161001learned-helplessness-and-the-languages-of-dao/
原理的には、コードは形式検証（formal verification）を用いて正しいことを証明することができる 。
：
これよりは苦労と厳密さが少なめで、ひいてはより有望なものの1つはlangsec構想だ：
LANGSECは、信頼できない入力を取り扱うソフトウェアを、信頼できるものにするための唯一の道は、すべての正しい或いは期待される入力を形式言語として取扱い、それぞれの入力処理ルーチンを、その形式言語への認識装置であるように取り扱うことだ、と想定している。
最善は善の敵である（最初から最善であることに拘ると、次善にすらたどり着けない）。私たちは現在の不名誉な状態から一足跳びに名誉ある状態に行くことはできない。
Language-theoretic Security
http://langsec.org/
