pasv VS cl-autowrap

Then you go to the more elaborate prover. We used the Boyer-Moore prover for that. After proving a implies b, that became a theorem/rule the fast prover could use when it matched. So if the same situation came up again in code, the rule would be re-used automatically.

I notice that the examples for this verified Rust system don't seem to include a termination check for loops. You prove that loops terminate by demonstrating that some nonnegative integer expression decreases on each iteration and never goes negative. If you can't prove that easily, the code has no place in mission-critical code.

Microsoft's F* is probably the biggest success in this area.[3]

[1] https://archive.org/details/manualzilla-id-5928072/page/n3/m...

[2] https://github.com/John-Nagle/pasv

[3] https://www.microsoft.com/en-us/research/video/programming-w...

This is a generic problem with macro systems, of course, which is why C deliberately had a weak macro system.

LISP is a blast from the path. It's fun for retro reasons, but things have moved on.

[1] https://github.com/John-Nagle/nqthm

[2] https://github.com/John-Nagle/pasv/tree/master/src/CPC4

> In the 70's, this wasn't considered a 'real' proof.

I ran into that decades ago. We used the original Boyer-Moore theorem prover [1] as part of a program verification system. The system had two provers, the Nelson-Oppen simplifier (the first SAT solver) to automatically handle the easy proofs, and the Boyer-Moore system for the hard ones. To make sure that both had consistent theories, I used the Boyer-Moore prover to prove the "axioms" of the Nelson-Oppen system, especially what are usually called McCarthy's axioms (the ones that use Select and Store) for arrays.

The Boyer-Moore system uses a strictly constructive approach to mathematics. It starts from something like Peano arithmetic (there is a number zero, and an operation add 1) and builds up number theory. So I added a concept of arrays, represented as (index, value) tuples in sorted order, and was able to prove the usual "axioms" for arrays as theorems.

The machine proofs were long and involved much case analysis.[2] I submitted a paper to JACM in the early 1980s and got back reviews saying that it was just too long and inelegant to be at the fundamentals of computer science. That might not be the case today.

A few years back, I put the Boyer-Moore prover on Github, after getting it to work with Gnu Common LISP. So you can still run all this 1980s stuff. It's much faster today. It took about 45 minutes to grind through these proofs on a VAX 11/780 in the early 1980s. Now it takes about a second.

The proof log [2] is amusing. It's building up number theory from a very low level, starting by proving that X + 0 = X. Each theorem proved can be used as a lemma by later theorems, so you guide the process by giving it problems to solve in the right order. By line 1900, it's proving that multiplication distributes over addition. Array theory, the new stuff, starts around line 2994.

The reason this is so complicated and ugly is that there's no use of axiomatic set theory. Arrays are easy if you have sets. But there are no sets here. Sets don't fit well into this strict constructive theory, because EQUAL means identical. You can't create weaker definitions of equality which say that two sets are equal if they contain the same elements regardless of order, because that introduces a risk of unsoundness. Effort must be put into keeping the tuples of the array representation in ascending order by subscript, which implies much case analysis. Mathematicians hate case analysis. Computers are good at it.

[1] https://github.com/John-Nagle/nqthm

[2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...

behave as if it does. The other extreme would be a GUI program.

[1] http://www.animats.com/papers/verifier/verifiermanual.pdf

[2] https://github.com/John-Nagle/pasv

which proves that the storing operation always produces a validly ordered array. That's essentially a code proof of correctness for a recursive function The Boyer-Moore prover was able to grind out a proof of that without help. That was a long proof, too.

I submitted this to JACM. It was rejected, mostly for uglyness. The concept that you needed all this heavy machine-driven case analysis to prove a nice simple "axiom" upset mathematicians. Today it would be less of an issue. People are now more used to proofs that take a lot of grinding through cases.

You could build up set theory this way, via ordered lists, if you wanted.

So that's a classic of what happens if you take "equal" seriously.

[1] http://www-formal.stanford.edu/jmc/towards.pdf

[2] https://theory.stanford.edu/~arbrad/papers/arrays.pdf

[3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...

[4] https://github.com/John-Nagle/nqthm

Some Common Lisp FFIs have opted to coax this information out of the compiler. https://github.com/rpav/c2ffi is a C++ tool that links to libclang-cpp and literally outputs JSON with sizes and alignments. (It is then used by https://github.com/rpav/cl-autowrap to autogenerate a Lisp wrapper.) The older CFFI Groveller [1] works by generating C code which is compiled by the system C compiler (e.g. GCC or Clang) and, when executed, prints Lisp code that contains resolved values of constants, sizes, alignments, etc.

[1] https://cffi.common-lisp.dev/manual/html_node/The-Groveller....

> Lack of access to the C libraries.

???

I recently started learning Common Lisp for fun (and fun it is!) and the ease of accessing C libraries was one of the things that surprised me in a positive way.

Using https://github.com/rpav/cl-autowrap one can simply write (c-include "file.h") and the API defined in "file.h" is accessible from Lisp. I can't think of a simpler way.

Even without cl-autowrap, FFI using https://cffi.common-lisp.dev/ seems simple enough.

I think the closest is cl-autowrap. I can imagine a higher level wrapper around it by which it can translate the python header file into the CL counterpart, although I'm not sure how much work the translation might entail. Also, because python and lisp semantics can differ considerably, the generated code might be trying to do weird things - again an issue of translation.

Common lisp has a "pretty OK" story for calling C code whenever some speed is needed [0,1]. In my opinion, they suffer from some of the documentation/quick start problems that common lisp has, but they're otherwise usable.

Some of Naughty Dog's late 90's/early 2000's games (Jak and Daxter, Jak II) were written in a lisp called GOAL, Game Oriented Assembly Lisp [2]

[0] https://github.com/rpav/cl-autowrap

The closest thing to what you request, that I'm aware of, is cl-autowrap (to use C code from Lisp) but it is not standard in any way. CFFI is the de facto standard for using C from Lisp across different implementations.

:claw tracks back to 2017 as a fork of cl-autowrap with cl-autowrap/pull/83 feature.

If you're interested in FFI, then yeah CFFI is the standard. The other comments addressed speed, I also wanted to point out https://github.com/rpav/cl-autowrap which is built on top of CFFI and can help get a wrapper up and running faster. After using autowrap's c-include you can then use CFFI basically like normal or some useful autowrap/plus-c's helper functions -- e.g. in one project, I have an SDL_Event (https://wiki.libsdl.org/SDL_Event) and to access event.key.keysym.scancode I have a helper function that's just (plus-c:c-ref event sdl2-ffi:sdl-event :key :keysym :scancode). Last year I wanted to try out using FMOD, and even though it's closed source and has a (to me) "interesting" API things worked easily: https://gist.github.com/Jach/dc2ec7b9402d0ec5836a935384cacdc... More work would be needed to make a nice wrapper, type things more fully, etc. but depending on the C library you might find someone's already done that (or made a start) and made it available from quicklisp.

In recent years there has also been cl-autowrap; caveats -

There is the cl-autowrap that can generate lisp packages from C header filesc- I am unsure if it sticks to ANSI C or goes beyond. It inturn depends on c2ffi for the first time around.