The seven programming ur-languages (2022)

Eh, no. You have Elisp+cl-lib but SBCL too, and you can use Sly wth SBCL.

Of Lem with SBCL+Quicklisp:

https://lem-project.github.io/usage/common_lisp/

Huge tip: if you use MCCLIM, install Ultralisp first and (ql-quickload 'mcclim) later: it will give you a big speed boost. Big, not as the ones from Phoronix. Actually big. From 'I can almost see redrawing on a really old ass netbook' to 'snappy as TCL/Tk' under SBCL.

https://ultralisp.org/

As you can see, you don't need to pay thousands of dollars.

For Scheme, S9 just targets R4RS but as a start it's more than enough, and for SICP you can install Emacs+Geiser+chicken Scheme and from any Linux/BSD: distro command prompt, you run:

       sudo  chicken-install srfi-203
       sudo chicken-install srfi-216

And, as a ~/.csirc file:

      (import scheme)
      (import (srfi 203))
      (import (srfi 216))

To run SCM stuff for SICP:

       csi yourfile.scm 

or

       chicken-csi yourfile.scm

Done. Get the SICP PDF and start doing SICP. You can use Emacs+Geiser with

         M-x install RET geiser-chicken

 if you are lazy. You can install the SICP book with

        M-xpackage-install RET sicp

and read it from

       M-x info RET

and do it everything from withing Emacs by running

      M-x geiser 

(pick chicken as the interpreter). Save your Emacs settings. Done.

"Cognato/a" in Italian is brother/sister-in-law

One correction I'd make to the article's taxonomy: Ruby is an object oriented language not an Algol. Its inspiration is Smalltalk, and much of the standard library naming comes from that route (eg collect rather than map).

Ruby is object oriented from the ground up. Everything (and I do mean everything) is an object, and method call is conceived as passing messages to objects.

While Ruby is most often compared to Python (an Algol), they come from very different evolutionary routes, and have converged towards the same point in the ecosystem. I think of Ruby as a cuddly Alpaca compared to Python's spitting camel.

> Agda, Idris, etc. are functional languages extended with complex types

I think they are not. No amount of type level extensions can turn a regular functional language like Haskell into something suitable for theorem proving. Adding dependent types to Haskell, for example, doesn't suffice. To build a theorem prover you need to take away some capability (namely, the ability to do general recursion - the base language must be total and can't be Turing complete), not add new capabilities. In Haskell everything can be "undefined" which means that you can prove everything (even things that are supposed to be false).

There's some ways you can recover Turing completeness in theorem provers. You can use effects like in F* (non-termination can be an effect). You can separate terms that can be used in proofs (those must be total) from terms that can only be used in computations (those can be Turing complete), like in Lean. But still, you need the base terms to be total, your logic is done in the fragment that isn't Turing complete, everything else depends on it.

I wrote something similar here: https://fmjlang.co.uk/blog/GroundBreakingLanguages.html

We agree on Algol, Lisp, Forth, APL, and Prolog. For ground-breaking functional language, I have SASL (St Andrews Static Language), which (just) predates ML, and for object oriented language, I have Smalltalk (which predates Self).

I also include Fortran, COBOL, SNOBOL (string processing), and Prograph (visual dataflow), which were similarly ground-breaking in different ways.