Background: @markm expressed an interest in a correct-by-construction methodology for writing the escrow service in Zoe 2. I made a spike to explore various approaches. (It also has more background and a bibliography of related research).
One of them is ACL2. (Dr. Boyer was one of my favorite profs at U.T. Austin. We’re still in touch from time to time, and he still strongly evangelizes ACL2.)
I made more tangible progress in dafny, but I hit a wall around promises and async stuff.
The other day, I wondered whether there are actor libraries for idris or ACL2. Then it occurred to me: goblins supports state transitions as pure functions. I could do it in goblins, and port the result to ACL2.
So I got started by taking the original 42 line escrow implementation from the 2013 paper and porting it to scheme: escrow2013.scm
I got as far as guix install guile-quickcheck, but then when I use c-x c-e on (use-modules (quickcheck)), it dies with no code for module (quickcheck).
I don’t see much about modules in the scheme primer.
Is Guile installed in your profile? You’ll need that in order to have the right shell config to source to get the necessary load path environment variables.
Alternatively, use guix shell:
dave@ikaruga ~$ guix shell guile guile-quickcheck
dave@ikaruga ~ [env]$ guile
GNU Guile 3.0.9
Copyright (C) 1995-2023 Free Software Foundation, Inc.
Guile comes with ABSOLUTELY NO WARRANTY; for details type `,show w'.
This program is free software, and you are welcome to redistribute it
under certain conditions; type `,show c' for details.
Enter `,help' for help.
scheme@(guile-user)> (use-modules (quickcheck))
scheme@(guile-user)> ,apropos quickcheck
(quickcheck): quickcheck-results #<procedure quickcheck-results (test)>
(quickcheck): quickcheck #<procedure quickcheck (test)>
(quickcheck): configure-quickcheck
scheme@(guile-user)>
does that guix shell trick work inside emacs, as an inferior scheme/lisp?
aha! found 10. Appendix: Setting up Guile, Wisp, and Goblins by way of a nearby post where somebody pointed out the link from the scheme primer to the heart of spritely. I’ll chew on that for a bit.
I recommend getting the basics working in a terminal, first, to keep the moving parts to a minimum. Integrating Emacs and guix shell is totally possible (I do it) but it’s a more advanced setup. Installing packages to your user profile is easier for starting with Emacs development.
Speaking of moving parts, I discovered Hall and kicked the tires. I didn’t have complete success, but it felt like it would eventually be cost-effective.
One clue was to get a complete set of devtools in one go: $ guix shell emacs emacs-geiser-guile.
The other was to import a bunch of modules that are implicit in the README:
(use-modules (quickcheck)
(quickcheck arbitrary)
(quickcheck property)
(ice-9 match)
(srfi srfi-26) ;; 26: Notation for Specializing Parameters without Currying
)
Figuring out this reverse-mapping from usage to defining module was tedious to say the least. I’m interested to learn how working scheme programmers do it as a matter of course. (IOU a separate thread.)
In JavaScript, the module system makes it statically evident where something was imported from. (It meets the lack of ambiguity requirement .) As a working JS dev, I use vs-code “go to definition” (F12). But even if I don’t have vs-code, I can do the reverse mapping manually without having to build an index of all the importable objects in the world.
p.s. My office hours notes include a tab-dump of related topics that came up during the discussion.
