定理証明手習い (64) テストと公理

コード書いたら動かしたいしせっかく動かしたら残したいので結局テスト的なものを書くことになります

(my/test "car/atom" (car 'a) '())
(my/test "car/cons" (car (cons 'a 'b)) 'a)
(my/test "cdr/atom" (cdr 'a) '())
(my/test "cdr/cons" (cdr (cons 'a 'b)) 'b)

公理に似ているものもありそうでないものもあり

(my/test "car/cons" (car (cons 'a 'b)) 'a)
(my/test "cdr/cons" (cdr (cons 'a 'b)) 'b)

は公理の証明の代わりみたいなもの
でも実装でなにか場合分けがあったりすると境界値でテストしないといけなかったり
考慮漏れがあるとテストが不完全になるのでカバレッジを計ったりするわけですよね
公理が証明できればこういうテストよりもずっと信頼性が高いわけだな

(my/test "car/atom" (car 'a) '())
(my/test "cdr/atom" (cdr 'a) '())

定理証明的には全域性に関わるテスト
こういうのは実装の詳細に関わることで、コード見てるからこういうテストが出てくるけど
あんまり大事じゃないのかな？
こういう場合、値はどうでもいいって言ってたな

(my/test "equal-same" (equal 'a 'a) 't)

これは公理だけど

(my/test "equal-differnet" (equal 'a 'b) 'nil)

これに相当する公理がなくて証明したいけどできないってことがあった
これはそういう公理は不要ってことなのか、この本では使う場面がないから出てこなかっただけなのか
これは値なんでもいいです、ってことはないはずだし

実際すごい信頼性が求められる分野でコードを証明しました！みたいなとこでは
何を証明しているんだろう？
どこまで証明すれば100%って言える？
信頼性が必要だからコードは証明しましたが公理（定理でもいいのか）が足りているかはわかりません、
ってわけには行かないような気がするし

それとも、望ましい性質だけを証明できればいいって考え方なのかな
（この本では使う場面がないから不要、的な）

たとえば、今定義しているj-bobが正しい結果を出してくれることを証明するとしたら？
(align/alignで死にそうになってるくらいだからj-bob自身で証明するのはとても無理そうだけど)