screwlisp<p><a href="https://mastodon.sdf.org/tags/formalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalMethods</span></a> <a href="https://mastodon.sdf.org/tags/gamedev" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>gamedev</span></a> <a href="https://mastodon.sdf.org/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>programming</span></a> <a href="https://mastodon.sdf.org/tags/commonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>commonLisp</span></a> <a href="https://mastodon.sdf.org/tags/acl2" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>acl2</span></a> <a href="https://mastodon.sdf.org/tags/itch" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>itch</span></a> <a href="https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">https://</span><span class="ellipsis">lispy-gopher-show.itch.io/lisp</span><span class="invisible">moo2/devlog/907091/formal-game-logic</span></a></p><p>Since yesterday I advocated strong use of defgeneric, defmethod and McCLIM's define-command, here I present </p><p>just giving lisp's defun to acl2's first order <a href="https://mastodon.sdf.org/tags/logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>logic</span></a>.</p><p>I present a batch processing style for using acl2 both in <a href="https://mastodon.sdf.org/tags/shell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>shell</span></a> and in <a href="https://mastodon.sdf.org/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>lisp</span></a> with a worked example.</p><p>Thoughts and opinions, gamedevs and logical types?</p>