It occurs to me that I do not have a signature online game. You might point
out that it has been a decade since I last played a game. An author named
Frank Sargeson observed that you had to be removed from a topic to see it
clearly... Anyway, I do not view my complete unfamiliarity with games as an
obstruction to me making a good one.
I figure a game needs to have state, controls, media, a clock and
networking. Since acl2 is my jam now, it should also be formally correct.
State is normally avoided in ACL2; being more simulation than an applicative
model [in fact, state transition is the opposite to being applicative].
Having a model having state transitions satisfies my ego.
Von Neumann bottlenecks are stobjs (single threaded objects) in acl2. Trendy
Haskell marketing calls them monads.
Pretty much finished amirite? Lists of sparse (game) objects and character
inputs for controls. I also decided to have cursors to acheive a for-each
for-each be part of the game state since they are basically about performing
state transitions sequentially. Viz for-each-for-each... Coming up with
particular theories of less than the implied O(nn) complexity is a side
goal.
My first hack at stateful input (without- lots of things) then. When you are
hell-bent on introducing stateful input to acl2, it has a special stobj
named state. I guess like Haskell's io monad.
Basically in :program (not :logic) mode also with no "soft error"(-tuple)
handling, but I get a character into the st ate stobj and from state into my
game-state stobj. Even without guard verification it is a little dance to
comply with the special von Neumann bottleneck handling (and the special
state stobj has more requirements still).
---
I saw jns has a game engine in his history somwhere. Inb4 I plagiarize
-Capability machine architectures
-Text justification
-Game engine
-???
Hopefully I add a something!