This is Hacker Public Radio episode 3,789 for Thursday the 9th of February 2023.
Today's show is entitled, Common List Portable Games including ACL2 Formologic.
It is the first show by new host's crew tape, and is about 54 minutes long.
It carries a clean flag.
The summary is describing exploratory liber common list portable games.
I am using ACL2 Formal Methods.
Alright everyone, one take, let's do this.
I want to call this show, ACL3, where the first ACL is going to be, what does I think of?
Alright, I've forgotten the first ACL, and the first A is going to be as stiff, which
is a system definition facility, and other system definition facility for common list.
Let me say, the C is code, and the L stand is taken from the word module.
So as stiff can compile modules of your common list system, and then the ACL2 that remains,
because I guess that 3 was an exponent, is Kaufman's ACL2, which is a computational
logic for applicative common list, which is an automatic in interesting senses, formal verification
tool.
So it helps you understand and reason about books of first order logic that you've defined,
and the primitive tools for this logic are a subset of our favorite language common list,
but only purely functional subset of it, except for single threaded objects, which are
this whole big thing, which would be monads in Haskell or ML.
And I have a slightly deviant approach to this, which is, what they're hoping that you'll
do, or what it says in their book, in Kaufman's, one of Kaufman's, maybe both of
Kaufman's, advances in formal methods books, where there are two of them, circa 2000,
about ACL2, where he emphasizes this, and you have to be kind of doing serious analysis,
like doing mathematical proofs, and the automatic part of ACL2, it's not automatic in
that it thinks of what you want for you, it can't do that.
What ACL2 can do is go at super-super-super-human speeds, checking that you haven't,
you haven't said something incompatible.
Yeah.
And the future will give a better definition than that, but that's how I think of it when
I'm wildly unprepared, and I've just turned on a microphone.
And so what the task that I kind of set for myself is someone showed me a cell phone game,
where you paint roads, and then there's some AI logic for cars that, once the roads are
connected, cars will spill out of one location, and it will try to, they'll each independently
try to follow a road to reach an exit location, their roads have been connected to.
And it seemed like a really fun kind of game.
The particular game I was shown doesn't really matter, and I don't intend to do anything
similar to it, but I really like this idea of having sources and sinks, and letting
the person paint with their finger or a mouse, a driveable or a navigable region, and then
having units try and traverse from the sources to the sinks, and giving them some notion
of simple AI.
And so where are we going with that, oh yeah, so I just wanted to make this as a game
in common list, which is why I've named this as the project car game, but I don't really
like cars or the widespread support of car infrastructure in our cities.
That's not what this show is about, but I'm renaming that car to be car from common
list, where if you think that a car has a car cell and a killer cell, yeah, maybe
it's car like that, I should explain more about as stiff, but let's talk about the car
game first, and in the future we can go into more detail about everything.
So listen to what I say in this episode, and then I'll address my many shortcomings.
Possibly in a formerly rigorous way, whatever the word formal means.
So in this car game, my premise for, oh, so I want things like, if I have well-defined
AI behavior, so some kind of simple AI behavior, and a road that's been painted in a
well-defined way, I would like to be able to prove true statements about the game and
the behavior of cars, roads, sources, and sinks in the game.
But at the same time, I would like to have a game, ideally that can be played on a tablet,
and you could paint roads with your fingers, basically, and then marble as units move along
your roads, and I don't know, you can have all the joy of civil engineering, I guess,
highway design, or like robot, walkway designs.
But these two goals are kind of at odds, in that playing a game is a very side-effecty
thing.
You know, the player can look at a picture, maybe a moving picture of what's happening.
There's a clock running, I guess, and the player issues controls whether they're
a culture mouse event, or keyboard inputs, which are all side effects, and for a wide range
of compilation targets, embeddable common list is a handy compiler, because it can slide
in anywhere that supports C and C is the thing that works everywhere.
So I had to reconcile how am I going to get formal theorems about my defense behavior,
define this, how you define a function in common list, and reconcile that with a playable
game, and maybe there are two approaches, and I went for one of them.
The approach I didn't go for is you can put basically any side effect you want, as long
as you have a monadic notion of it, you can have streams and files and stuff in ACL2's
un-noyman state object, it's more primitive way of just representing single threaded
states, but instead of trying to cram everything into ACL2, because I'm being so badly
behaved already, I wanted to have in my system definition, I'm going to have one module,
which is files in a subfolder of your list system, and have that be the defense, and have
the rule all the funds to common list function or process definitions have to be in that
module, and they all have to be admissible in ACL2, so ACL2 in order to do its automatic
checking, will only accept functions that are total, there's a well-behind, well-defined
behavior for any input it can get, and the input has to be able to be anything, that's
not actually very important, but anyway, you have to handle all possible inputs that the
defined can get, and it has to have a well-defined output as well, and a handy if sometimes
elegant feeling, way to do this is a bit basically instead of having iterators, you're going
to use recursion, cal recursion, which has some efficiencies, as you know, and the recursion
has to clearly terminate at some point, if it doesn't look like the recursion will definitely
terminate, the function won't be admitted, and some of the kind of built-in theorems and tools
of ACL2, not a built-in book, but kind of primitive to the system, it's very good at telling
that inferring simple measures, so you might have two lists as the argument of a defined,
and say, well, if either of them is not a proper consp, which is an ACL2 recognizer for
non-empty true lists, which they have, what's called guards, which are a way of cutting away
great swaths of possible erroneous inputs. So ACL2's recognizer, proper consp, will deal with anything
that isn't a list, and that isn't a non-null true list, and yeah, so we've got these two lists,
and we've dealt with all the non-list cases somehow, or we're dealing with them, I guess, and
a really easy measure would be if you're emptying one list into the other, and then the measure
could be the length of the list you're emptying, and if every recursion that list
loses its front element, I guess we wouldn't say pop, because that sounds kind of side-effecty,
but the recursion might be that it moves the car of the second list into, it just
depends it to the first list, and then recurses now with the one shorter second list, and then when the second list
is no longer a proper consp to return the first list, and so that would be an example of a recursive
function, so a non-trivial function, with a measure that we didn't have to specify ourselves,
in that we're just draining one list into another list, and it goes by at least one every time,
and once the list is empty, it's the recursion is over, so we have an exit condition there,
I guess, which is important to our well-defined recursion, herbs are trying to go with this,
yes, so the defunds are all going to be kind of like that, and they're going to be all right,
because commonless compilers like everyone, I guess, know about tail recursion,
because iteration, you would have to prove a lot about what iteration means, but what recursion means,
is pretty clear, including mutual recursion, maybe, so I had to start putting together what kind of
defund tools I'm going to need for my card game, which all of the logic should be in these
defunds, I wanted all the logic to really be ACL2 lists, even though I'm using it in commonless,
so I have to, I have to port the definitions of ACL2 primitives out of ACL2 and back into common,
that's before for things like that proper currency, and ACL2's documentation, because ACL2 was
implemented in commonless, they have, for your reference, how they defined everything in ACL2 in
commonless, but there's not just defunds, so I have another module, which is side effects,
and the side effects, that is, the side effects deal with all the side effects, and the defunds
module, deals with all the defunds, and there's also a macro-start list, which is the first thing
that loads, and I decided the macro-start list will kind of buy its nature, it will be acceptable
to ACL2, because macros don't really do anything, as long as you have a well-defined
commonless macro, did I have anything else, let me type LS, and look at what's actually in my
credit, oh not this file, oh and then so I've got a folder, which isn't really a module, because
it's not, it doesn't do anything, there would be no value, or from the carcatgame.st, the
list system definition file, this folder is unnecessary, but this ACL2 folder is kind of where
the magic happens with ACL2, you have them there as well, and it's normal to have a package
just not list to include your package definitions, because your package definition and your
system definition are obviously different things, so that's that, and I'll have a repeat.org,
I've got one kind of sitting there in this folder, which I need to clean up, but I'll put on my
on my go-for-flog over on STF's BST server there, which you can reach from my go-for-flog
STF-flog, which is a go-for log, I guess, how are you listening to me if you don't know what that is,
no of you're listening to hacker public radio, hopefully. Ask someone else, ideally ask me,
could ask me on my mastodon, and you could find me via hacker public radio, or via STF, but I'm
really kind of every man side of the STF mastodon, not the cool kid side,
so what are we going to look at? I'm not just going to read code, but I am going to think
just try and wax a little miracle about what are the defunds I have at the moment, so all of these
are well-defined and can be admitted as this module, so it's a common list,
as the three module for a common list game, but given the package, the nickname ACL2 user,
which is the default user package name within ACL2, which also has these package names faces,
I guess, and so normally the package is actually a miscar game, but then in the file that in the
files that can be certified as ACL2 books, I'm just going to refer to the car game package as
ACL2 user, just as a kind of heristic there for me, it might be a more beautiful way of doing that,
if you know one tell me, but that's what I'm figuring out. So my defund, sort of API, I guess here,
all of the functions operate on what I've been calling Stodge, so single threaded object,
so Von Neumann State object, I guess, but actually these Stodge's are just, oh so Stodge
would be moaned in some other languages, but the Stodge is really just a common list association list,
which is just a list, and its members, if it's not mill, are all conses, and I think they just
have to be, the members are conses, that's really the condition, and these are used for
there are simple to reason about way of categorizing data and replacing data in that you just
make a new A-list association list by adding something onto the front, and if that thing on the front,
if the car of the cons was already in the A-list, you just, you just terminate the first time you
find a name, so you can update previous entries by just adding an entry with the same car to your A-list.
If this is ambiguous, you know, tell me, and we'll work on that. Well, I'll all listen to this,
and the second episode might be better, or might be worse, who knows. So I have a reset that just
makes an A-list that is kind of, it's prepared to have, for it's got a cons of the name,
notes, and a cons of the name robots, and a cons of the poorly named last note, which is actually
like what the next note key should be, because I was kind of using increasing number key identifiers
for the different notes, then I have a defined name add note, which adds a note to a
large A-list, and so that A-list, so it takes an A-list, which is implicitly going to be the
cutter of the notes in the A-list, and returns it with another note of the rowing column, and it will
also get the key of that note from this last note, and increase that last note. And so it's a
state-full way of operating, but secretly, this single threaded objects are acceptably functional,
they're well defined in some kind of way. So we have that add note, and we have a get note from
ID and the A-list, where we'll get the note, or mill if it doesn't find it, I guess, and it will
just search for the note from the front of the A-list, so that when the note is updated, it can just be added
to the front again, and only the front most one will be found. Then I had clean A-list, which
is something I shouldn't have done, so it's like my guilty admissions, first episode, that would
been a way better name for this show, guilty admissions, but clean A-list, which I had this function
just to delete A-list content that wouldn't be reached anymore. So well, it's interesting to have
that stuff, because it gives you an actual history of changes that have been made. If some very
deep recursion was happening, or lots of updates had happened, I was worried that this A-list
would get too big during some of the automatic proofs, so I added this clean A-list, that takes
an A-list that has members that will never be accessed again, and gets rid of them, and then I also
had D-dupe IDs, which was really just clean A-list, but specifically for notes, so that notes
that had been changed, it just kind of cleans out the old ones. Right, I think this is a mistake,
because I have to do a whole bunch of proof work to show that these functions basically aren't
doing thing dangerous, but I just do think that they will give me some performance optimization
in groups, which might be desirable, because I didn't talk about that. I wanted to talk about that.
But when sort of disagreement, I have with everyone else about A-CL2, is I'm not very interested,
and I've actually read some other people talking about this as well, so who knows how derivative
my ideas are here. If you compare Coke, which is like, so C-O-Q, which is a proof assistant,
and it's a very watchful pen and paper, where instead of using a pen and paper, you express yourself
to Coke and Coke doesn't do anything automatically, but it does, well, I guess, automatically,
but in a different sense, keep tabs on whether you've said something that's obviously
incompatible with the previous ideas that you were laments, I guess, that you've said it.
And that's not the behavior, so I guess A-CL2 does do that, and that's how you're meant to be thinking
about A-CL2. What I like is that the process of A-CL2, no, not the process, the automatic process
inside A-CL2, will do things that you could never possibly do yourself, and it's not that I want
to have a regular proof assistant, and do regular proofs, and sometimes it accelerates me a little bit,
by doing things I couldn't voluntarily, automatically, doing things I couldn't possibly have done
myself. I'm really, really specifically interested in, in gendering behaviors that I can't
possibly do myself, and then I can just feed all of the hard work, the Kaufman will, if Kaufman
ever hears my voice, he'll be unhappy with me for saying this. Directly into A-CL2, my challenge
is to speak in a way that A-CL2 automatic components understand easily, and then train myself
to do the minimal amount of work to trigger an A-CL2 behavior, and then I don't want to know anything
about what A-CL2 can do for me. I just want to know how a few good, heristic approaches to just
doing my own minimal amount of work, and maximize the amount of work A-CL2 does, which there's
some pitfalls to my approach, but yeah, this was kind of my theory, where I wanted to not do anything
recognizable as trying to use a pen and paper to do the proof myself. I purely want to reach
a state where A-CL2 will get my vibe and do a proof in a way that I wouldn't have been
been able to do it, and then we'll kind of gather those together and, and well, we will show some
things are true about my car game. I should mention, for people who aren't familiar with computational
logic, or first-order logic. So, a way that I think it's useful to present formal proofs,
formal in some sense. Formalists, everybody's kind of ashblub about the word formal, or the word
formal is not a very formally defined word. It kind of means serious, I guess, or robust. It can
be seen as as being different to regression testing, or if not regression testing. So, regression
testing is where you write a test of your program. So, your program has, there was a mistake
found in your program, and you write a test that should trigger the mistake. You fix the mistake,
but every time you update your program, you read on these tests to make sure you haven't
reactivated that mistake or gotten to that mistake state again. So, this is the testing approach.
And people also then try to imagine mistakes that they might make before they make them, which is
not a very robustly defined approach to imagine things that haven't gone wrong, but maybe
could go wrong. So, I would refer to this as ad hoc testing. I think I've seen referred to it as
if you want to argue with me about my language. You're very welcome to
write about it on your go-for-flog or contact me on Macedon or somewhere like that.
Oh, I'm screw-taped incidentally on go-for and on Macedon. So, I would be, I guess, at screw-taped
Macedon.stf.org. In my vlog would be go-for.club-1-users-scrutate.
All right, I think I've just been rambling at you for half an hour. Do you think I'm just going to
upload this one no matter no matter what it's like? We did eventually. I think I got these the order of
these topics a little bit wrong because I wanted to try just doing this off the couple of staring at a
directory or at my commonless system definition directory here.
What are the defunds? So, I had add exit because the point of these notes. So, I was imagining this card
in where I'm just making arbitrary decisions here, but I'm kind of trying to choose low hanging
fruit for things to prove theorems about. So, I have all these notes and they're in the
cutter of an A list and they are themselves another A list with numeric keys, I guess.
And then, so I wanted the kind of players screen or what they're interacting with just to be a
regular or the linear non-dense, I guess, I need to say that space, space of notes and the
ideas these notes can have exits to each other. So, it might be exits to its nearest neighbors,
but the exits could really go anywhere. So, one of the nearest neighbors might not be connected.
So, it's, I would describe this as a hyper grid. So, I have a simple A list notion of a hyper grid.
And then, oh, did I say non-dense? It might be very non-dense in the future if the hyper grid only
exists where a road has been painted. Yeah, and, and so, I have a defined that takes the old
notes list and adds an exit from some node ID to another node ID and then it returns
the A list with that node updated. So, I have a way of, so I have a list which is a single threaded
object which is kind of static and then I'm adding notes to it and then I have a notion of connecting
these nodes with this add exit and I have my regretful pseudo-efficiency witchcraft. And then,
I just had a few utility functions for reciprocal connections and for just making rectangular grids
recursively. So, while some people have books pre-made in robust books made in ACL2 for
reasonable iteration and you can also use common lists array syntax even though it's secretly
being represented as as a list inside ACL2. Yeah, I decided to use a non-dense A list here.
Right, so I did all of that and then what were my side effects going to be and I could over
rep open this file. I can't remember if I did anything in this. Oh, that's pretty cool.
I'll push to picture this on my go for and master them for you to look at.
So, because I realized in many ways I was redoing one of my implementations of the land of
list while this hunt, which is a great common, less learning, learning book and land of the
last witch, but what's his name going to be? SCM recommended to me.
Well, having a hybrid grid was kind of, I guess it wasn't necessarily a grid, but these
hyper connected nodes, where a hyper means the connections can do anything, not just go to
locations next to each other and there can be any number of them, that kind of stuff.
So, because of that, I had a side effect. Oh, that is actually a defund. I guess I used defunds in the
side effects as well, but they're kind of side effect defunds. I'll think about
whether that's kind of robust. So, I guess they're a logical defunds and then they're
pure side effect defunds. So, this defund, which I seem to have named dot-stog, which is a bad
name, because that's not really what it does, uses very non-ACL to come in lists loop macro, to
to print a graph that is dot, kind of directed graph visualization, textual definition, using column
lists string formatting, and then turns that into into a KNG potentially, or any other output
that dot has, then another side effect I see here uses FET, which is my preferred image viewer
to show you the visualization that has been made. So, those are some nice side effects.
I was also, so they should get their own module, but I was also having in the side effects,
the definitions of ACL2 primitives that aren't in common lists. There are definitions in common
lists, as in a sufficiently accurate way. I don't think these are exactly like proper
consp, I have a definition, but I didn't actually, oh, yeah, this was the embarrassing
admissions show, and what do I have? So, for proper consp, I've just quickly defined that to have
roughly the right behavior approaches, and so if it's a function of an object, I have end
odd consp, no color last odd. Oh yeah, and so that end odd means that it's a non-null object,
has to be a consp and has to be a true list, so the color of the last element of the list
has to be null, so it's a, I think that makes it a true list. It's probably a better
way in common lists to represent that, than I also had ZP, which is an ACL2 guarded version of
ZP that I've just got doing ZP there, and I know you're thinking, maybe this could have just been
a half hour show, even though we've gone for 40 minutes already, but they ACL2 folder in my list project.
Where I'm hoping that you, you install common lists, maybe ACL, if you wanted to distribute
something like my game here on C supporting platform, so Android or Apple Objective C or
same environment, like open BSD or net BSD or free BSD or Linux, can see the belief if one must.
Okay, let's, let's quickly talk about those dependencies then, and so I had to build ACL2 myself,
but just on the environment, I'm staring at right now, it's an MD64 open BSD and
and still bank common lists has been ported to AMD64 open BSD, and so I just, you know,
package at SBCL as my common list, oh actually I guess, oh yeah, so I'm using two different common lists,
I've used SBCL with ACL2, where SBCL is just kind of faster in a lot of in general than
then embedible common lists, though the actual, the actual game projects will be built with
ACL, which is also, ACL is super portable, it doesn't have like the harsh, kind of, or dangerous
kinds of memory access that the SBCL requires for speed, so what happens, I think SBCL uses
M map in a way that open BSD is not always very content with, whereas ACL just makes normal
C programs and open BSDs can deal with that in a happier way, where was I going with this?
Yeah, and then I just downloaded and built ACL2 with SBCL, and so that's, that's the ACL2 I'm using,
and if you're on DBN, DBN definitely already has ACL2 built, though I think DBN's normal
ACL2 package has been built with canoe, common lists, or C list, I guess that one's normally called.
It's, C list been GCL the same thing, yeah, I'm going to say there are, so on DBN, I guess you
would just act install ACL, or ACL2 sounds pretty easy, and then I guess you would also just act
install ACL, or if you're on open BSD like me, I guess package and ACL.
And then, then you're where I am, I guess if you had, I'll have a script somewhere for downloading
my package, I kind of play coy with, with not having gets for things, because for one,
and I realize that it uses a bare git repository for, um, as it's kind of storage object.
On open BSD, we would normally use game of trees rather than rather than get.
Where game of trees has useful behaviors, where as git, the historical git has every behavior
under the sun, and that's too complicated for simple-minded open BSD, a simple-minded open BSD user,
such as myself. Anyway, we're going to run out of time if I just keep, keep talking at you,
but so let's talk with this ACL2 sort of data folder that I've also got in the project,
and so I think it's really exciting thing. There's a make file, and this is a little, a little bit tricky,
which I'm probably breaking some some norm of ACL2 here, so I basically wanted to have
uh, my ACL2 book certification. I wanted to shell script it, so I wanted to create these ACL2
certified and compact books, um, as an automatic side effect when I'm, when I'm doing other things.
So I have a shell script, which I mean, you're invoking ACL2 in, in your shell, right?
So there's no reason you can't just, um, do that ACL2, and then, uh, left angle bracket,
left angle bracket, the OG, and then just put all of your, or, or, or you would just pipe, sorry,
just use standard input and pipe, um, pipe the file that, uh, I don't know, I guess, I guess you wouldn't do that.
So, so you could do what I said in the first place. I should actually look at this.
We, what do I name this? I'm gonna say, it's named ACL2. That's, all right, ACL2,
um, angle bracket angle bracket. I've got what that's called in, in shell. So the shabang is just been
SH, um, and I'm doing ACL2, angle bracket, angle bracket, and double-pote, OG, and then I just have my, my
purely functional ACL2 certification, um, just being piped into ACL2, and, and when we reach the,
the end of file, or, OG again, quotes, OG, it just ends. And so I guess I include book,
car game. Oh no, I must, I have a second thing for sure to find this. So this assumes we've already certified
car game. I think I have that in the read, me, because I wanted to make people do the certification by hand,
because that's the responsible thing to do. Anyway, include book, card, car game,
impackage ACL2 user, which from, uh, from ACL2's perspective, it believes that it's actually just
using the ACL2 user default user package. But ACL2 user was actually earliest to card game in the
as if three system definition. So that's, that's a little bit of chicaneary. I'm, I'm guilty of
again there. And what is it doing? I guess it deaf stogges, um, a stogge, and then I have a trivial
theorem, which is a one by N, uh, a one by N nodes, uh, space, um, in my ALS node sense. The number of nodes
will, will be N, which, well, that that was just my, my example theorem. And it's a little bit
tricky because, uh, what I found is so far, I haven't used guards effectively enough. So I have to
prove a lot of things are true about ALS, which if I'd, uh, written in slightly better form ACL2,
I'll already, I think, has theorems about what's going on with an ALS. But I was having, um, difficulties
with, uh, guarding out streams. So I think there are places where, where a string could be put,
and it would lead to a weird behavior. It's a work in progress. This shows work in progress.
Let's go see if I have, oh yeah. So anyway, that's, I guess the reason that, that shell script is
called ACL2 test is that it was a test theorem in, in ACL2, just to exhibit ACL2 being driven
automatically by SH. It's the make file. Oh yeah. So I, I've just got make, uh, make all, I guess, and make
clean, which cleans out, uh, the old compiled ACL2 book certification in a way that you're not meant
to do. But this was a quick hack. Um, then I have macros. Oh, oh, this is where it's being certified.
I see. Man, I should have looked at this before before, turning on my mic. So macros and macros
just pipes certified book macros to ACL2, which, which will then assume there's no error,
certified book macros. Um, and then car game, which just print F's. Oh, which in, yeah,
print F's include book macros, new line, certified book car game one, because there's only one,
um, one thing in macros, and pipes that to ACL2. And then copy list, which in all,
actually happens before those two book certifications, uh, copies, the car game dot list, the, the
defense file, um, into, into the ACL2 data directory, and also copies macros top list.
Oh, yeah. So, so it just copies those two source files that are using the nick game ACL2 for car
game, um, and then it certifies them, uh, just just as amazing SH1 liners, I guess. And then
test afterwards, which is it runs that ACL2 test. I rambled about a little bit. This is kind of
the set of tools that I'm working with at the moment for, um, for, on one hand, I want to just
make a game, except make a game really applicatively. So I have that explicit separation.
Oh, I'll eventually use, um, STL2, which I quite like, for, um, STL2 is a reasonably low level
cross-platform high level. I kind of, it has a notion of mouse events and, and keyboard events and,
and game controller events and, um, touch events and, and graphics. And they're, uh,
uh, extensions for, for high level audio and, and loading images as well for it. And so I kind
of want to have this, and so that STL2 stuff, um, which, which I think might be, it might be, I
want to do portably. But I could do it with, um, the commonest CFFI package, maybe. I'll think about it.
But I, I like to just write ESCAL because, um, it's more transparent what's happening, but, uh,
that binds us to, to only loading that system in ESCAL. Um, so I think I'll do more episodes of
this as well. And after I've listened to this one, though, I might just try batting my eyelids
at hacker public radio and seeing if they'll take this if they consider it up to snuff.
I'm going to look at what I think needed more exposition, or I just got flat wrong in, in, uh,
in the event. I managed to notice that. And, um, build on my approaches to, to making, making games.
I guess, specifically for mobile devices, but I'm, but also kind of free to me device, like,
normal environment. So you don't have to worry very much about making a game for normal environment.
But, um, yeah, just making, uh, C-like, elf games, and, um, in common, let's,
but doing it in a modular approach with, with as if three, um, in, in a way that the
applicative, the logical parts of the game are also certified as ACL2, first order, logical,
um, less books. Yeah, so, so I, I just, I would like everyone to have the capacity to do those two
things. Um, clearly, I would benefit greatly from some feedback here. So, if you are normally a
web person, do hit me up on at screw tape, at mastodont.stf.org, or if you're, if you're in the go for,
hopefully I, I already am aware of you, but you can also join the go for, um, which might be,
might be my, my non-radio show, with a list of go for show, um, where that one is, is about,
kind of go for community news, and, and come and list, not covered by, um, by anything else I'm doing,
uh, whereas I'm gonna keep trying to submit these ACL2, but kind of quirky ACL2,
athletic, but with a different meaning, if you were it after the, athletic, if meaning, I'm
applying it to, to making side-effecty games, um, ACL2, automatic proof, certified book, um,
programs. All right, I think, hopefully we're out of time. I'm turning off the mic. Thank you, everyone.
I love you all. Good bye. Feel free to give me feedback if you would like my next show,
have a higher standard, or if you, if you're participating, uh, if you're already an ACL2 expert,
you might have some guidance or harsh criticism to share with me, and, um, I welcome that enthusiastically,
or you might want to make some games, and further, makes some games that you have some
first order logic, proven behaviors out of. But you don't want to do all the work. You want
to do even more work to trick ACL2 into doing things. You kind of know how to do yourself,
but, but it's funer to make ACL2 do things. There's a lot of value to that, I promise.
All right, goodbye. When cloudy, I am, um, engendered me to do this. I haven't actually
listened to cloudy on shows yet, but that's on my, on my to-do list for today. I was going to record
one of these cold and then try listening to cloudy on cloudy on. All right, goodbye, going. I love you all.
You have been listening to Hecker Public Radio at Hecker Public Radio.org. Today's show was
contributed by a HBR listening like yourself. If you ever thought of recording podcasts,
you click on our contribution to find out how easy it means. Hosting for HBR has been kindly provided
by an onsthost.com, the internet archive, and our sing.net. On the satellite stages, today's show
is released on our creative comments. Attribution for going to international license.