Pasv Alternatives

pasv reviews and mentions

• Why Is Common Lisp Not the Most Popular Programming Language?
  8 projects | news.ycombinator.com | 14 Feb 2024

  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

• Will Computers Redefine the Roots of Math?
  6 projects | news.ycombinator.com | 30 Jun 2023

  > 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...

• What I've Learned About Formal Methods in Half a Year
  3 projects | news.ycombinator.com | 10 Apr 2023

  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

• Grothendieck's Approach to Equality [pdf]
  2 projects | news.ycombinator.com | 30 May 2022

  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

• A note from our sponsor - InfluxDB
  www.influxdata.com | 28 Apr 2024

  Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality. Learn more →