プログラム利用時のすべてのユース・ケース を 完璧に網羅 する 検証テスト なんてありえない！ なら、「論理的」に「プログラムの正しさ・完璧さ」 を 証明する「定理証明支援系言語」か？ ～ その関数型言語 との関係 - Qiitaプログラム利用時のすべてのユース・ケース を 完璧に網羅 する 検証テスト なんてありえない！ なら、「論理的」に「プログラムの正しさ・完璧さ」 を 証明する「定理証明支援系言語」か？ ～ その関数型言語 との関係形式証明定理証明CoqAgda関数型言語 この記事は、「形式証明」や「定理証明」を行うプログラミング言語とその使い方について調査を始めた作業メモです 400年の難問、「ケプラー予想の証明」やっと100％終わる コペルニクスが提唱した地動説を、天体運行法則で不動のものにした偉人ヨハネス・ケプラー。 そのケプラーが1611年に提唱した「球は、八百屋に山盛りのオレンジみたいにピラミッド型に並べると一番沢山入る」という説が、400年の歳月を経て、100％正しかったことがコンピュータの力で証明されました。 この立体最密充填の解答は、誰でも直感的になんとなく正しいことがわかります。けれども証
