181351 posts 1993 follows 1215 followers
Please pay attention to random failures.
ACL2 でブラックジャックの勝敗判定を実装してみた。Lisp だけど全ての関数が停止することを証明しているし、重要な関数の戻り値が期待したものになることも証明している。静的型付けとは異なる証明への道へ歩み始めた。
https://gitlab.com/tojoqk/blackjack/