Post #1819341
2026-04-28 07:10 UTC
@simon_brooke
Oh that would actually be so cool. ACL2's famous case study was hardware verification of floating point operations for the motorola 68k series (er, iirc). It would be neat if you verified your hardware with it (as a case study!).
@vnikolov
Replies (1)
-
@simon_brooke@mastodon.scot 2026-04-28 07:18
@screwlisp @vnikolov If I can get the system to a stage where I can port packages from other Lisps to it that will be a big win. My idea is that I will have at least a #Clojure read table and a #CommonLisp read table -- but because the underlying structure is slightly different from either, porting most things will probably need a little rewriting. Still, ACL2 is now on that list!