ACL2 でブラックジャックの勝敗判定を実装してみた。Lisp だけど全ての関数が停止することを証明しているし、重要な関数の戻り値が期待したものになることも証明している。静的型付けとは異なる証明への道へ歩み始めた。
https://gitlab.com/tojoqk/blackjack/
lambda のない Lisp を Lisp と呼んでいいのか謎
@tojoqk@mastodon.tojo.tokyo LISPはいいぞっ
@tacumi LISP 最高ですね!
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!
lambda のない Lisp を Lisp と呼んでいいのか謎