(軽量)形式手法の補足
ここからは(軽量)形式手法に関する補足なので、それ自体を知っている方 or 関心が出なかった方は読まなくていいです。
形式手法とは
形式手法とはソフトウェアの品質保証のための、数学的・記号論理的手法の総体
記号的であるため計算機実装が可能
形式手法の例
- 形式検証 verification
- 自動生成 synthesis
- 形式仕様記述 specification
TL;TD;
ここでは型システムをプログラムに関する推論のためのツールだとみなしている。
軽量(light weight)形式手法
実際の開発に携わる人々の中には、形式手法コミュニティが仕様記述と設計の完全な形式化を強調しすぎていると感じている。彼らは対象となるシステム自体の複雑性だけでなく使用する言語の表現能力が完全かどうかが形式化を困難にしていると主張する。代替案として様々な軽量（ライトウェイト）な形式手法が提案されてきた。それらは部分的な仕様記述と応用に注力したものである。このようなライトウェイトな形式手法の例として、型システム、uppaal Alloy オブジェクトモデリング記法、Z言語によるユースケース駆動型開発、CSK VDM ツールセットがある。
- 型システムは軽量形式手法の1例である。
- 型システムを使った開発は、形式手法の水準1だとみなしている
2. wikiの形式手法の水準１に書かれている「形式手法を使って開発と検証」の例に「詳細化と属性の証明」がある。つまり、コードを書いて、コンパイルを通す事と同義。 - Coqで証明駆動開発して、Extractionする開発手法が水準2だと思っている
形式手法を調べたら、非形式主義的という言葉が出てきた。
水準0
形式仕様記述を行い、プログラム自体を非形式主義的に行う。「軽い形式手法」と呼ぶ。費用対効果が早く得ることができる選択である。
そもそも形式主義とはなんだろうか？ 
一般に事物の内容よりも形式を重んずる立場。ものごとの形式を重んじてそれにこだわり、内容を軽視もしくは無視する立場。また、その考え。
- 数学用語としての形式主義 - 形式主義 (数学)
なるほど、数学用語なんですね。
つまり、水準0は、プログラム自体は「内容よりも形式を重んずる立場ではない」が、形式仕様記述は行う。この組み合わせは費用対効果が高いらしい。
ここでまた1つ知らない用語が出てきた。
形式仕様記述とはなんだろう？
形式仕様記述（けいしきしようきじゅつ、英: formal specification）とは形式手法のひとつで、何らのシステムなどについて、その性質などの仕様を形式的に記述する手法や、そういった手法による仕様の記述である。
「その性質などの仕様を形式的に記述する」 => プログラミングにおいては、データの型(形式)に関してそこまで書かないが、アルゴリズム等は記述する必用のある、スクリプト言語とかが合致しそうですね。
形式的な仕様を与えることにより、対象システムが仕様に照らして正しいかどうかを形式的に判定することが可能となる(形式的検証)。また、仕様策定の工程で仕様の不整合を検出することが可能となり、実装工程のような開発の後半での仕様不備発覚、それに伴う手戻り(多大なコストを要する場合が多い)を防ぐという利点がある。他の使われ方として、仕様から設計、設計から実装へと段階的に検証可能なステップを踏んで詳細化し、開発工程で不具合を作りこむのを防ぐ。
「形式的な仕様を与えることにより、対象システムが仕様に照らして正しいかどうかを形式的に判定することが可能となる」 => つまり、型を書くことにより、型システムでの検査が可能になり、型システムの仕様に照らして正しいかどうかを形式的に判定することが可能となる。