>>1さんよ、

Coqという言語を使えば、集合論を含む数学の証明や、プログラムの性質や品質保証ができるらしいぞ。
やってみないか？