Idrisで依存型を使った定理証明入門 | κeenのHappy Hacκing Blog

このエントリはIdris Advent Calendar 2020の19日目の記事です。 次はmock_beginnerさんでIdrisとはじめる型駆動開発です。 κeenです。今回はこのAdvent Calendarの山場の1つ、定理証明について解説しようと思います。 依存型で証明ができる原理 カリー＝ハワード同型対応といって、プログラムのと論理学の定理には対応関係があることが知られています。 これはすなわち、我々が普段プログラムを書いているときは同時に論理学の命題を証明していることでもある、ということです。 そんな大それたことしてないよーと思うかもしれませんが、それもそのはず。 普通のプログラムではあまり面白い命題を表現できないので、わざわざ証明というほどでもないからです。 しかしIdrisには依存型があります。 依存型があると型の表現力が上がるので対応する論理学の命題の表現力が上がり

[mizchi]

“証明さえあれば数個の値で挙動を確かめるいい加減な方法（テストと呼ばれます）よりずっと確実に正しさを保証できる”