One   of  my  projects   this  week  has  been  writing    a
road-painting   game which will eventually  surface  in some
form, largely at the prompting of my brother a few weeks ago
but I am just getting to it now. 

Perhaps  only to my own and ratxue's delights,  it continues
my exploration  of maverick  acl2. To resemble  my brother's
idea,  I'm  writing  it for compilation  targets   that  ecl
matches. 

QUICK CLARIFICATION OF ACRONYMS

acl2  is an *automatic*  theorem  prover;   a  computational
logic   for an applicative subset of common lisp 

ecl embeddable common lisp is a common lisp compiler that is
just a C library, libecl.  Since C is ubiquitous,  this is a
way of easily  getting common lisp programs *anywhere*  such
as  if  one desired  it, the proprietary  apple store,   the
proprietary  steam store, the proprietary  google store  for
example  if this was the only way to get the program onto  a
non-free  device.  If you wanted to embed ecl in golang, one
could   compile   the  ecl to a C lib and use the C  lib  in
golang,  which is supported.   The big C dependency  is  the
Boehm garbage collector.  ECL conses quite a lot, leaning on
garbage collection. 

END OF CLARIFICATION

An idea that came to me was the reusability  of theorems  to
infer  truths you couldn't  personally  reach,  the  magical
value-adding  of acl2's automatic  nature implying   natural
feature reuse. 

Imagine  that a game is a collection  of capabilities  and a
puzzle where the puzzle contents  and capabilities  imply  a
way of reaching  the next level.   defthm  the idea that the
player has the capability  to reveal unknown locations,  and
has  some  unknown  locations  that if revealed   allow  the
character to reach the next level. So I could do some higher
level reasoning about a space of games using the same lemmas
- imagine the memory card-flipping game, or cutting grass in
a walking  simulator  in order  to find a dropped key.  This
would be cooler if I had implemented these already, but this
was an exciting conceptual discovery for me. 

Call the capabilities  acl2-compatible  lambda forms and the
game  state an acl2 single  threaded  object  acted upon  by
those  lambda  forms.  Then I could have a theorem  about  a
permuted  set of features  I hadn't personally  thought   of
putting together that the character has the capabilities  to
act on the level (single threaded  object) to advance in the
game. 

Single threaded objects in acl2 are a generalisation  of its
early  von neumann state in theorems,  used in some examples
with a non-canonical #'seq acl2 macro which is essentially a
forward pipe operator 

(seq stobj do-this then-this and-this finally-this)

As used in

:doc stobj-example-1

#|addendum
If for some reason you know R, imagine magrittr
(I'm not going to explain R's implementation but arbitrary
strings can be new infix operators) bad analogy:

> add-1 "%>%" add-2 "%>%" add-3 "%<%" 4
10

the number four was a stobj here ;p
|#

This pushes  me to jettison  non-acl2  common  lisp, such as
progn forms (though seq is basically that) and my dear clos.
The exploration continues.