Sage @sage

0 posts0 participants0 posts today

**screwlisp** @screwtape@mastodon.sdf.org · Mar 17

screwlisp @screwtape@mastodon.sdf.org

#formalMethods #gamedev #programming #commonLisp #acl2 #itch https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic

Since yesterday I advocated strong use of defgeneric, defmethod and McCLIM's define-command, here I present

just giving lisp's defun to acl2's first order #logic.

I present a batch processing style for using acl2 both in #shell and in #lisp with a worked example.

Thoughts and opinions, gamedevs and logical types?

itch.io(formal) game logic - lispmoo2 by screwtape1. Intro This begins part 2 of https://lispy-gopher-show.itch.io/lispmoo2/devlog/906389/my-programming-principles-for-game-dev-12 . Which contains the first five parts. These second five parts contain...

Replied in thread

**screwlisp** @screwtape@mastodon.sdf.org · Aug 17, 2023

Aug 17, 2023

screwlisp @screwtape@mastodon.sdf.org

@arialdo what's the problem being observed? Though it's a normal example case in automatic proof assistants like #acl2 how it can take hundreds of steps to sketch
(thm
(implies (and (true-listp list) (equal rrlist (rev (rev list))))
(equal rrlist list)))

Replied in thread

**screwlisp** @screwtape@mastodon.sdf.org · Jun 3, 2023

Jun 3, 2023

screwlisp @screwtape@mastodon.sdf.org

@awkravchuk @rwxrwxrwx
#acl2 definds #'+ as a macro like this:
(defmacro + (&rest rst)
(if rst (if (cdr rst) (xxxjoin 'binary-+ rst)
(cons 'binary-+ (cons 0 (cons (car rst) nil))))
0))
where 'binary-+ adds/guards two number arguments. So I guess there's that (+) -> 0 again ;p