pasv VS awesome-cl

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

I know you're not asking for recommendations, but Lisp, particularly SBCL, really seems to check all your boxes. I say this as someone who generally reaches for Scheme when it comes to Lisps too.

There are a few game engines[0] for CL, but most of them seem to be catered specifically to 2D games.

[0] https://github.com/CodyReichert/awesome-cl?tab=readme-ov-fil...

Hello, a single counter-example I hope https://lispcookbook.github.io/cl-cookbook/editor-support.ht...

(see more from https://github.com/CodyReichert/awesome-cl?tab=readme-ov-fil...

https://cl-community-spec.github.io/pages/index.html

and some more)

Everyone, if you don't have a clue on how's Common Lisp going these days, I suggest:

https://lisp-journey.gitlab.io/blog/these-years-in-common-li... (https://www.reddit.com/r/lisp/comments/107oejk/these_years_i...)

A curated list of libraries: https://github.com/CodyReichert/awesome-cl

Some companies, the ones we hear about: https://github.com/azzamsa/awesome-lisp-companies/

and oh, some more editors besides Emacs or Vim: https://lispcookbook.github.io/cl-cookbook/editor-support.ht... (Atom/Pulsar support is good, VSCode support less so, Jetbrains one getting good, Lem is a modern Emacsy built in CL, Jupyter notebooks, cl-repl for a terminal REPL, etc)

check out the editor section, there's more than Emacs these days: https://lispcookbook.github.io/cl-cookbook/editor-support.ht...

- https://github.com/CodyReichert/awesome-cl for libraries

- https://www.classcentral.com/report/best-lisp-courses/#ancho...

- a recent overview of the ecosystem: https://lisp-journey.gitlab.io/blog/these-years-in-common-li... (shameless plug, on HN: https://news.ycombinator.com/item?id=34321090)

More HTML generators for CL: https://github.com/CodyReichert/awesome-cl#html-generators-a... there are lispy ones (Spinneret), Django-like ones (Djula, I like it, easy to use and extend), HTML-based allowing for inline Lisp code (Ten), JSX-like ones (lsx, markup), and more.

https://github.com/CodyReichert/awesome-cl is usually a good place to find recommendations. Jzon is pretty good.

> obstacles add up

I actually agree. It wasn't smooth for me to ship my first CL app. It's all better now (more tools, more documentation, more blog posts from several people, more SO questions and answers!).

> performant

SBCL is in the same ballpack of C, Rust or Java in many benchmarks.

In this article series, the author writes the same program in CL, Rust and Java. In fact, he copy-pastes a PG snippet from 30 years ago. This snippet beats Rust and Java in LOC and speed. But, yeah, he wasn't writing super efficient Rust code, so after many discussions, pull requests and sweating, the Rust code became the most performant. https://renato.athaydes.com/posts/revisiting-prechelt-paper-... It didn't take work to make the CL code performant, more so for the Rust one ;)

a benchmark after sb-simd vectorization: https://preview.redd.it/vn5juu36v2681.png?width=715&format=p... (https://www.reddit.com/r/Common_Lisp/comments/riedio/quite_a...)

> good tools for networking, for writing concurrent or asynchronous code, for graphics,

I refer the reader to https://github.com/CodyReichert/awesome-cl but yes, CL won't have the best libraries in some scenarii (GUI? Tk libs are good, we have Gtk4, a Qt5 library used in production© by a big player but difficult to install etc)

> it doesn't give you a good package manager or means of distributing code

Quicklisp is neat, with limitations, that can be addressed with Qlot, ql-https, or CLPM or the newest ocicl.

It's a good book!

Modern companions would be:

- the Cookbook: https://lispcookbook.github.io/cl-cookbook/ (check out the editors section: Atom/Pulsar, VSCode, Sublime, Jetbrains, Lem...)

- https://github.com/CodyReichert/awesome-cl to find libraries

Also:

- https://stevelosh.com/blog/2018/08/a-road-to-common-lisp/

- https://news.ycombinator.com/item?id=34321090 2022 in review

> static strong typing

Alright, here is it: https://github.com/coalton-lang/coalton/

> small efficient native binaries

The numbers are: with SBCL's core-compression, a web app with dozens on dependencies will weight ±30 to 40MB. This includes the compiler, the debugger, etc. Without core compression, we reach ±150MB.

> The actor runtime?

the actor library: https://github.com/mdbergmann/cl-gserver

> couldn't find a way to make money with it. I suspect many other programmers are in my boat.

Alright. Some do, that's life. Yes, some companies go with CL even in 2023 (https://lisp-journey.gitlab.io/blog/lisp-interview-kina/, they released https://github.com/KinaKnowledge/juno-lang lately; Feetr (finance): https://twitter.com/feetr_io/status/1587182923911991303)

https://github.com/azzamsa/awesome-lisp-companies/

> Give us an HTTP (1.x & 2.0) and WebSockets libraries

How so? We have those libraries. HTTP/2: https://github.com/zellerin/http2/

https://github.com/CodyReichert/awesome-cl

https://leanpub.com/lovinglisp -- this one is great, and the first thing I recommend

https://lispcookbook.github.io/cl-cookbook/ -- also great and up to date

https://awesome-cl.com/ -- for anything else.