nqthm VS pgloader

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

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 have played with nqthm, which was last modified in 1992. Only a few modifications were needed to get it to load from Quicklisp, one amusingly was because LaTeX changed over time, so the LaTeX generator had to be changed slightly.

No, it's difficult to read, and understand. It's a parenthesis circus, example -

https://github.com/dimitri/pgloader/blob/master/src/sources/...

Examples (for Common Lisp, so not citing Emacs): reddit v1, Google's ITA Software that powers airfare search engines (Kayak, Orbitz…), Postgres' pgloader (http://pgloader.io/), which was re-written from Python to Common Lisp, Opus Modus for music composition, the Maxima CAS, PTC 3D designer CAD software (used by big brands worldwide), Grammarly, Mirai, the 3D editor that designed Gollum's face, the ScoreCloud app that lets you whistle or play an instrument and get the music score,

but also the ACL2 theorem prover, used in the industry since the 90s, NASA's PVS provers and SPIKE scheduler used for Hubble and JWT, many companies in Quantum Computing, companies like SISCOG, who plans the transportation systems of european metropolis' underground since the 80s, Ravenpack who's into big-data analysis for financial services (they might be hiring), Keepit (https://www.keepit.com/), Pocket Change (Japan, https://www.pocket-change.jp/en/), the new Feetr in trading (https://feetr.io/, you can search HN), Airbus, Alstom, Planisware (https://planisware.com),

or also the open-source screenshotbot (https://screenshotbot.io), the Kandria game (https://kandria.com/),

and the companies in https://github.com/azzamsa/awesome-lisp-companies and on LispWorks and Allegro's Success Stories.

https://github.com/tamurashingo/reddit1.0/

http://opusmodus.com/

https://www.ptc.com/en/products/cad/3d-design

http://www.izware.com/mirai

https://apps.apple.com/us/app/scorecloud-express/id566535238

I worked on migrating our MySQL system to PostgreSQL using pgloader ( https://pgloader.io/ ).

There were some hiccups, things that needed clarification in documentation, and some additional processes that needed to be done outside of the system to get everything we need in place, it was a amazing help. Not sure the project would've been possible without it.

Data mapping from PostgreSQL to PostgreSQL as in the article isn't nearly as bad as going between systems. We took a full extended outage and didn't preload any data. There were many dry runs before hand and validation before hand, but the system wasn't so mission critical that we couldn't afford to shutoff the system for a couple of hours.

Initially, I started down the pgloader path, which seemed to be a common approach for the database conversion. However, using my M1-chip MacBook Pro led to some unexpected issues. Instead, I opted to use NMIG to convert MySQL to PostgreSQL. For more information, please check out the “Highlights From the Database Conversion” section below.

I just checked pgloader (which is mostly for heterogeneous database migrations) and it doesn't seem to have any explicit throttling features, either. However, you can set concurrency, number of workers, and batch size.

But do what makes you happy. The best PostgreSQL data loader in the world is written in Common Lisp. Now, CL is a fast and ANSI standardized language with multiple implementations, and was used to create Reddit, but it's hard to call it fashionable.

- [ScoreCloud](https://scorecloud.com/) - A web and mobile application to automatically create music notation from music performance or recordings. Built with LispWorks.

## DB tools

- [Pgloader](https://github.com/dimitri/pgloader/) - Migrate to PostgreSQL in a single command!. [PostgreSQL License]

I would warmly recommend https://pgloader.io but, unfortunately, the Oracle support is still in need of a sponsor :-)

I followed instruction here: https://github.com/dimitri/pgloader/blob/master/INSTALL.md, but can't get pass sbcl requirement.

https://pgloader.io/ There's been a great tool available for this for many years.