We got to build mini versions of the first 4 languages (imperative, lisp, ML, Smalltalk) in the PL course at tufts which is now published as a textbook [1]. There used to be a prolog part that sadly got cut.
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.
Since Python introduced new style classes, it also became a pure OOP language, even though it might not look like it at "Hello World" level, all primitive types have become objects as well.
I have found the definition of OOP to be fuzzy. For example, I don't see why having methods would make a data type object oriented. I associate OOP with factories, inheritance, using classes in places that might be functions otherwise, and similar abstractions.
Perhaps this is the counterfactual: I program in Python regularly, but don't program in an OOP style; I use dataclasses and enums as the basis, in a way similar to Rust, which by some definitions can't do OOP. So, if Rust can't do OOP (assumption) and I can write Python and Rust with equivalent structure (Assumption), does that mean Python isn't strictly OOP?
Rust can definitely do OOP, not only I could easily convert "Raytracing in one Weekend" from C++ into Rust, while keeping the same design, Microsoft has no issues adding a Rust projection for COM/WinRT, which are OOP ABIs.
However that is not the same as Python, which is 100% OOP, when using basic stuff like numbers, from Python language semantics those things are object, and there is the whole machinery in place even for basic stuff like addition.
And yes OOP is fuzzy from CS point of view there are multiple approaches and it doesn't get reduced to the way C++ and Java do it, just like FP and LP are fuzzy as well.
Some folks would swear if it isn't Haskell or Prolog, than it isn't FP or LP, when a CS book and programming language evolution will be more fuzzy.
That seems like a pretty lame gotcha--saying "Aha! The language you write in uses your hated paradigm under the hood" seems to invite the immediate response of "So? I don't use it."
I think the choice to identify a specific ur-language as "Object oriented" throws people off since OO is just a style of programming in the same way that procedural is. I don't think it's useful to say that Python and C++ are both the same kind of language because they both have multiple inheritance, rather that's just an observable commonality, like noticing that both Delhi and Vegas are too hot. Yeah, but I don't think that's because they're the same kind of place...
Object-oriented programming is less of a syntax and more of a philosophy. While Erlang’s syntax belongs to the ML family, its creator, Joe Armstrong, argued that Erlang aligns more closely with the original OOP philosophy defined by the inventor of Smalltalk than Java does: 'The essence of object-oriented programming is messaging, not classes and inheritance.'
I might add another class of languages: those intended to express proofs, via the Curry-Howard correspondence. Lean is a primary example here. This could be considered a subclass of functional languages but it might be different enough to warrant a separate class. In particular, the purpose of these programs is to be checked; execution is only secondary.
> 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.
This is just wrong, you're being too didactic. Idris specifically lets you implement nontotal functions in the same way that Rust lets you write memory-unsafe code. The idea is you isolate it to the part of the program with effects (including the main loop), which the compiler can't verify anyway, and leave the total formally verified stuff to the business logic. Anything that's marked as total is proven safe, so you only need to worry about a few ugly bits; just like unsafe Rust.
Idris absolutely is a general-purpose functional language in the ML family. It is Haskell, but boosted with dependent types.
Random passerby chiming in: so this means you can write "regular" software with this stuff?
While reading TFA I thought the theorem stuff deserved its own category, but I guess it's a specialization within an ur-family (several), rather than its own family?
It definitely sounds like it deserves its own category of programming language, though. The same way Lojban has ancestry in many natural languages but is very much doing its own thing.
Yes Idris was meant to write regular code. F* is also meant to write regular code
But I think that the theorem prover that excels most at regular code is actually Lean. The reason I think that is because Lean has a growing community, or at least is growing much faster than other similar languages, and for regular code you really need a healthy ecosystem of libraries and stuff.
> if you're a developer who wants to exploit the multiplicative factor of a truly flexible and extensible programming language with state of the art features from the cutting-edge of PL research, then maybe give Lean a whirl!
Does not sound that appealing to me. Sounds like little consistency and having to learn a new language for every project.
> 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
What I meant is that the part of Idris that lets people prove theorems is the non-total part
But, I think you are right. Haskell could go there by adding a keyword to mark total functions, rather than marking nontotal functions like Idris does. It's otherwise very similar languages
> 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).
Despite what the fanatical constructivists (as opposed to the ones who simply think it's pragmatically nice) seem to want us to think, it turns out that you can prove interesting things with LEM (AKA call/cc) and classical logic.
I mean you are kinda right but kinda wrong. To get a proof checker you take a typed lambda calculus and extend it with Pi, Sigma, and Indexed Inductive types while maintaining soundness.
Yes haskell's bottom breaks soundness, but that doesn't mean you need to take away some capability from the language. You just need to extend the language with a totality checker for the new proof fragment.
Lean is definitely a dependently typed ML-family language like Agda and Idris, so "ML" has it covered. And the long-term goal of Lean certainly is not "execution is only secondary"; Microsoft is clearly interested in writing real software with it: https://lean-lang.org/functional_programming_in_lean/Program...
OTOH if you really want to emphasize "intended to express proofs" then surely Prolog has that covered, so Lean can be seen as half ML, half Prolog. From this view, the Curry-Howard correspondence is just an implementation detail about choosing a particular computational approach to logic.
These are not true programming languages because by definition they are not Turing complete. If they were Turing complete it would be possible to write a false proof that just compiled down to a non-terminating program.
I feel like Turing completeness has always been set as the boundary of programming language if there's any boundary at all. That's what people has been using to not include HTML as programming language for example. Or to include MTG as one.
I think it's a pretty recent thing. Turing completeness is neither a sufficient nor a required property.
HTML is not a programming language, it's a markup language - it's in the name, and it's the way it is used (it's not used to describe any kind of computation, it's straight up data that is parsed by algorithms).
Neither is PowerPoint, or game of life a programming language even though both are Turing complete.
Turing completeness is the upper bound of computability, not the lower bound. It's useful mostly for showing that some thing can express the full range of computable problems, or for snarking that some thing is far more complex than it has any right to be.
Total languages omit partiality and non-termination from Turing completeness.
Partiality is IMO irrelevant when it comes to computability. Any partial function (that is, one whose range is not defined over its whole domain) can be expressed as a total function by either constricting the domain or expanding the range. For example, a "pop" operation on a stack is not defined for an empty stack. You can just loop forever if pop() is called on an empty stack. Alternatively, you can require that pop() is given a witness that the stack is non-empty, or you can require that pop() returns either the top-most element of the stack or a value that indicates the stack was empty. Both let you compute the same set of things as the former.
Non-termination is required to be Turing complete, because being Turing complete means being able to compute functions that one cannot reasonably expect to complete before the heat death of the universe. In _practice_ every function terminates when the computing process dies due to some external factor: process runs out of memory ("real" Turing machines have infinite memory!), user runs out of patience, machine runs out of power, universe runs out of stars, that sort of thing, so _in practice_ doing 2^64 iterations before giving up will generally* give you the same outcome as doing an unbounded number of iterations: it'll either terminate, or the process will be killed (here, due to reaching its iteration limit).
On the flip side, giving up non-termination and partiality only gives you increased correctness. If there's one thing we've definitely established in computing, it's that we will readily discard correctness to gain a little extra productivity. Why make a developer implement code to handle reaching an iteration limit when you can just make the user get sick of waiting and kill your app?
* 18 quintillion is a very large number. Have a try. The most trivial recursive function, on my M4 Mac, when convincing clang to be smart enough to turn it into a loop but dumb enough not to elide it altogether, would take a bit shy of 600 years to complete if iterating ULONG_MAX times; I didn't wait for that, if I'm honest with you, I ran it with a much smaller iteration count and multiplied it out.
I recently revisited a language comparison project, a specific benchmark tallying the cycle decompositions in parallel of the 3,715,891,200 signed permutations on 10 letters. I kept a dozen languages as finalists, different philosophies but all choices I could imagine making for my research programming. Rather than "ur" I was looking for best modern realizations of various paradigms. And while I measured performance I also considered ease of AI help, and my willingness to review and think in the code. I worked hard to optimize each language, a form of tourism made possible by AI.
Naively this is quite surprising, but the devil is in the details. With the exception of Lean I'd point out they're all fairly close: Chez being 2.5x slower than C++ is not ignorable but it's also quite good for a dynamically-typed JITted language[1]. And I'm not surprised that F# does so well at this particular task. Without looking into it more closely, this seems to be a story about F# on .NET Core having the most mature and painless out-of-the-box parallelism of these languages. I assume this is elapsed time, it would be interesting to see a breakdown of CPU time.
I don't think these results are quite comparable because of slightly differing parallelism strategies; I'd expect the F# implementation of just spinning off threads to be more a little more performant than a Rayon parallel iterator, which presumably has some overhead. But that really just shows how hard it is to do a cross-language comparison; Rust and C++ can certainly be made faster than the F# code by carefully manipulating a ton of low-level OS concurrency primitives. This would arguably also be little misleading. Likewise Chez and Haskell have good C FFI; does that count? It's a tricky and highly qualitative analysis.
[1] FYI, one possible performance improvement with the Chez code is keeping the permutations in fxvectors and replace math operations with the fixnum-specific equivalent - this tells the compiler/interpreter that the data are guaranteed to be machine integers rather than bigints, so they aren't boxed/unboxed. I am not sure without running it myself, but there seems to be avoidable allocations in the Chez implementation. https://cisco.github.io/ChezScheme/csug/objects.html#./objec...
Thank you. I will try your Chez idea. I love Chez, even if coding in Scheme can feel like rubbing sticks together to start a fire on an island, when e.g. Scala has induction ranges. And I didn't try Idris or Racket as they compile to Chez, but perhaps they do so better than I did.
As for parallelism this is a primary concern of mine, and I tried multiple approaches for every language where there was a choice. I used my own work-stealing code only when it beat standard libraries. AI warned me I was in over my head, that writing such a library takes years of experience, but my use case (and my expected use cases in my research) is so uniform that simple can win, minimally touching the required bases such as permuting tasks to avoid false sharing.
I don't believe that the JIT languages (F# on top) do so well because of better parallelism. This is branch optimization. For this use case an AOT compiler with ample benchmark data to influence output should do better. That isn't a thing, and the argument seems to be that few use cases stay consistent. A JIT can adapt.
Yeah :/ For a larger program you can pay the readability toll once, via a syntactic form that expands the general vector/arithmetic operations to the fixnum versions, e.g. used something like
(define (heap-permute! perm j callback)
(with-context 'fixnum ;; same trick works with 'flonum for 64-bit floats
(let ([n (length perm)]) ;; actually fxvector-length
(let generate ([k (- n 1)]) ;; actually fx-
(if (< k j) ;; fx<
(callback perm)
(begin
(generate (- k 1)) ;; fx-
(do ([i j (+ i 1)]) ;; fx+
((>= i k)) ;; fx>=
(if (even? (- j k)) ;; fxeven?, fx-
(swap perm j k)
(swap perm i k))
(generate (- k 1)))))))) ;; fx-
Sorry if I borked the indentation. I have been working on stuff like this, and more general macros around dependency injection and inversion of control (e.g. you could write this macro to take the type as a parameter and generate code optimized for 'bigint or 'rational). Maybe check back after the summer :)
And BTW I misspoke earlier, of course Chez is AOT rather than JIT. From one approach it's sort of a hybrid: really fast on-the-fly AOT kinda looks like JIT, tongue-in-cheek you could say "NoT compilation" (nick-of-time). But proper JIT of course has huge advantages. If you reeaaaallly wanted to sabotage readability, Chez makes it easy to invoke the compiler at runtime, so along with the C FFI I think you could hack together some sort of JIT. But wow, what a mess that would be! You'd better be getting a PhD thesis out of it :) And if the performance is that critical you'd be much better off with F#.
I haven't looked into the code, but Lean being so slow may be misleading depending on how you benchmarked it. IMO the fairest test is how "Lean code" (or Rocq code, etc.) is actually run, which is as native C code following extraction.
Given the sane C defaults that are applied by code extraction techniques, the delta really shouldn't be so great. But it's a common pitfall to torture one's own verified code in order to get it proven, and I'm also not sure how good of support there is for parallelism.
there's a few more semantic families: verilog, petri nets and variants, Kahn process networks and dataflow machines, process calculi, reactive, term rewriting, constraint solvers/theorem provers (not the same with Prolog), probabilistic programming,
plus up and coming (actual production-ready) languages that don't fit perfectly in the 7 categories: unison, darklang, temporal dataflow, DBSP
It may feel like a little bit of cheating mentioning the above ones, as most are parallel to the regular von Neumann machine setup, but was meaning for a while to do an article with 'all ways we know how to compute (beyond von Neumann)'.
> was meaning for a while to do an article with 'all ways we know how to compute (beyond von Neumann)'.
Would be very glad to read this.
In the meantime, I reproduce a part of an article by Steve Yegge:
---
What Computers Really Are
Another realization I had while reading the book is that just about every course I took in my CS degree was either invented by Johnny von Neumann, or it's building on his work in mostly unintelligent ways.
Where to start? Before von Neumann, the only electronic computing devices were calculators. He invented the modern computer, effectively simulating a Universal Turing Machine because he felt a sequential device would be cheaper and faster to manufacture than a parallel one. I'd say at least 80% of what we learned in our undergrad machine-architecture course was straight out of his first report on designing a programmable computer. It really hasn't changed much.
He created a sequential-instruction device with a fast calculation unit but limited memory and slow data transfer (known as the infamous "von Neumann bottleneck", as if he's somehow responsible for everyone else being too stupid in the past 60 years to come up with something better. In fact, Johnny was well on his way to coming up with a working parallel computer based on neuron-like cellular automata; he probably would have had one in production by 1965 if he hadn't tragically died of cancer in 1957, at age 54.)
Von Neumann knew well the limitations of his sequential computer, but needed to solve real problems with it, so he invented everything you'd need to do so: encoding machine instructions as numbers, fixed-point arithmetic, conditional branching, iteration and program flow control, subroutines, debugging and error checking (both hardware and software), algorithms for converting binary to decimal and back, and mathematical and logical systems for modelling problems so they could be solved (or approximated) on his computing machine.
I volunteered to do the formula parser, thinking it sounded like a fun challenge.
I was stumped for a week, until I realized I could rewrite the formulas into a form I knew how to parse. So it would rewrite 1+1 into ADD(1,1) and so on.
I also refused to learn regex, so the parsing code was "interesting" ;)
I recall a comment from a colleague. "Okay, Andy says it works. Don't touch it." XD
Guy from another group used regex and his solution was 20x shorter than mine.
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.
My favorite subject when studying CompSci (TU Delft) was called "Concepts of programming languages". We learned C, Scala (for functional) and Javascript (prototypes).
It made learning Elixir years later much easier.
We also had a course that basically summed up to programming agents to play Unreal Tournament in a language called GOAL which was based on Prolog.
For years I've wanted to use Prolog but could not figure out how. I ended up making a spellcheck to allow LLM's to iterate over and fix the dismal Papiamentu they generate.
Reminds me a bit of Bruce Tate’s approach in 7 languages in 7 weeks, which is where I first encountered Erlang.
I think from a historical perspective, describing COBOL and Fortran as part of the ALGOL family is a stretch, but I suppose it’s a good reminder that all history is reductive.
C++ has Algol roots, but I think the C++ template metaprogramming style is an ur-language of its own. You could draw some parallels with ML maybe, but they came at it from a different direction.
This article is full of gross mistakes. For example it claims that Caml is "Cambridge ML" which is ridiculously false. Fact check every sentence. Really sad.
I always enjoy these summaries. I took my bachelor of computer science in the early 1990s. It covered a language in most of these categories.
We didn't learn APL (Who is teaching the use of those custom keyboards to 100s of young students for one semester?)
The processing power of systems at the time made it clear which language classes were practically useful and usable for the time and which were not.
Prolog ran like a dog for even simple sets of logic.
We had the best internet access and pretty powerful desktop systems for the time.
I'm still curious why we didn't learn smalltalk. Could have been the difficulty of submitting and marking a system in a particular state rather than a file of code :)
Lots of us are having fun identifying our choice for missing family :)
One I might suggest is scripting languages, defined loosely by programming tools which dispatch high-level commands to act on data pipelines: sed, AWK, the sh family, Perl, PowerShell, Python and R as honorary members. In practice I might say SQL belongs here instead of under Prolog, but in theory of course SQL is like Prolog. Bourne shell might be the best representative, even if it's not the oldest.
AWK et al share characteristics from ALGOL and APL, but I feel they are very much their own thing. PowerShell is quite unique among modern languages.
I agree with "learn different classes of languages". OCaml was a language in which finally a function was a (mathematical) function. Mathematica thought me to look at expressions themselves as inputs. PostScript (with its reverse Polish notation going beyond simple arithmetics) rewired by brain.
At the same time, I don't agree with that it does not matter if one picks "Java, C#, C++, Python, or Ruby". If your goal is to do quick sort, then well, it does not.
If you want to use language for something (not only for its sake), then it makes a day and night difference. A person who wants to do 3D games and being shown Ruby or a person wanting to do exploratory data science and deep learning and being given Java are likely to get discouraged.
I used to think being an engineer meant learning many languages. Turns out most of them solve the same problems — the returns diminish quickly. Depth across the stack (UX, CI/CD, model internals) compounds in a way that a sixth language never will.
I wonder if Occam is worth a mention? It doesn't feel like anything else here, and is playing with its hardware synthesis descendants on a FPGA is another "mind expanding" paradigm.
Most old-timers here are familiar with a Prolog-variant: make. Anyone who's struggled over a complex Makefile wishes they had a more sane declarative language!
Folks might find the following useful for studying PLs;
1) Advanced Programming Language Design by Raphael Finkel - A classic (late 90s) book comparing a whole smorgasbord of languages.
2) Design Concepts in Programming Languages by Franklyn Turbak et al. - A comprehensive (and big) book on PL design.
3) Concepts, Techniques and Models of Computer Programming by Peter Van Roy et al. - Shows how to organically add different programming paradigms to a simple core language.
> "What do I mean when I say fundamentals? If you have an array or list of items and you’re going to loop over it, that is the same in any imperative language."
Err
"Fortran: The world’s first programming language standard opened the door to modern computing"
For any other array language novices, I've experimented with K and J but had the best experience so far with BQN. It is a bit on the Lispy side like K but much better documented, and I thought the APL-esque symbolic alphabet was mnemonically helpful enough while reading code to justify learning an editor keyboard integration. (Plus it's fun.)
I’ve very slowly been trying to do the “99 problems” list in each of these languages groups. It’s been a fun experience seeing the differences. Though I think I would need a larger, less algorithmic, project to really see each group’s strengths. Especially for the OOP group.
One thing the article didn’t touch on was SmallTalk’s live visual environment. It’s not a normal source code / text language.
- Forth: you can use PFE,Gforth for ANS Forth requeriments.
Or EForth if you reached high skills levels
where the missing stuff can be just reimplemented.
EForth under Muxleq: https://github.com/howerj/muxleq
I can provide a working config where a 90% of it
would be valid across SF.
If you follow the instructions on compiling s9, mlite it's similar
with MinC for Windows. If you are a Unix/Linux/Mac user, you already
know how to do that.
You got the whole docs in the TGZ file, and the web.
I would add another to the list, which is languages where every expression yields zero or more values, particularly jq. there are some antecedents in Icon and xquery, but these generally require explicitly opting into either production or consumption of value streams, where jq does this stream processing automatically from the ground up. (icon requires use of a suspend and needs an every clause to walk the generated values, xquery requires explicit 'for' statements over streams as many builtin operators fail on value streams)
in jq, the comma separates expressions, which independently yield values. a span of such expressions is called a 'filter', since they are always run by passing values from the prior filter into them (with the initial values sourcing from json objects on stdin, or an implicit null if you pass -n to the program).
binding variables in the language is similarly done for each value their source yields
$ jq -nc ' (1,2,3) as $A | $A + $A '
2
4
6
functions in the language are neat because you can choose to accept arguments as either early bound values, or as thunks, with the former prefixed with a $.
for example, this runs . + 100 parameters context, with . as the 10,20,30 passed to it:
in the world there should only be one debate and one summary about programming languages, and everybody should read that as a starting point before they enter the fray.
for example, I would say what i was taught, that lisp is lists made out of cons cells, which contain references to either other lists/cons cells or to atoms. lisp doesn't "have" parentheses any more than lisp has the rest of the ASCII table, but parentheses were chosen as a convenient way to write list structure down in ascii form because parentheses nest in exactly the way lists do and lists are the important thing.
then there never needs to be another discussion of parentheses and how you feel about them except in a sub-discussion if anybody has any bright ideas about alternative ways to convert list structure to ascii on paper. you disliking parentheses does not mean you dislike lisp; it just means you don't understand lisp, like for instance you think lisp has something to do with ascii.
similar ideas apply to C, wherein the braces and semicolons do not matter, what matters is datatypes that correspond to von neumann architectures including especially pointers, and where binary representation is easily exposed (with a syntax that does not matter but for the record is &, |, ~, ^, <<, or >>. if you hate those choices for operator syntax you could easily convert your own C to use parenthetical lists of CamelCase names of LeftAddRight or whatever floats your boat instead of a + sign), just keep in the front of your mind how data is represented internally and how it's mapped to the syntax you like, and whatever list structure you choose to order the lines of code)
Ur-ness is not interesting, just as the city of Ur was no doubt a lot less interesting than the city of Rome. Study Algol only to learn about call-by-name, then forget it.
I could go on, but, like the ripples from a gold coin thrown in the bay, the effect will soon dissipate as if I had never written anything at all.
155 comments
[1]: https://www.cambridge.org/ir/universitypress/subjects/comput...
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.
I love to point this out to OOP haters,
Perhaps this is the counterfactual: I program in Python regularly, but don't program in an OOP style; I use dataclasses and enums as the basis, in a way similar to Rust, which by some definitions can't do OOP. So, if Rust can't do OOP (assumption) and I can write Python and Rust with equivalent structure (Assumption), does that mean Python isn't strictly OOP?
However that is not the same as Python, which is 100% OOP, when using basic stuff like numbers, from Python language semantics those things are object, and there is the whole machinery in place even for basic stuff like addition.
And yes OOP is fuzzy from CS point of view there are multiple approaches and it doesn't get reduced to the way C++ and Java do it, just like FP and LP are fuzzy as well.
Some folks would swear if it isn't Haskell or Prolog, than it isn't FP or LP, when a CS book and programming language evolution will be more fuzzy.
> if Rust can't do OOP (assumption)
Rust handles basic OOP, but not all of the characteristics seen in C++ or Java:
https://doc.rust-lang.org/book/ch18-01-what-is-oo.html
Yes.
I wonder if my formal university python training predated this change (~2010), or if the professors were themselves unaware of this.
https://gnosis.cx/publish/programming/metaclass_1.html
https://www.python.org/download/releases/2.2/descrintro/
> I love to point this out to OOP haters
That seems like a pretty lame gotcha--saying "Aha! The language you write in uses your hated paradigm under the hood" seems to invite the immediate response of "So? I don't use it."
> Aren't camels a Perl thing?
That's a deep cut. :-)
For anyone reading this, O'Reilly was once legendary for their cover-art mascots.
- Agda, Idris, etc. are functional languages extended with complex types
- Isabelle, Lean, etc. are functional languages extended with complex types and unreadable interactive proofs
- Dafny etc. are imperative languages extended with theorems and hints
- ACL2 is a LISP with theorems and hints
Related, typeclasses are effectively logic programming on an otherwise functional/imperative language (like traits in Rust, mentioned in https://rustc-dev-guide.rust-lang.org/traits/chalk.html).
> 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.
Idris absolutely is a general-purpose functional language in the ML family. It is Haskell, but boosted with dependent types.
While reading TFA I thought the theorem stuff deserved its own category, but I guess it's a specialization within an ur-family (several), rather than its own family?
It definitely sounds like it deserves its own category of programming language, though. The same way Lojban has ancestry in many natural languages but is very much doing its own thing.
But I think that the theorem prover that excels most at regular code is actually Lean. The reason I think that is because Lean has a growing community, or at least is growing much faster than other similar languages, and for regular code you really need a healthy ecosystem of libraries and stuff.
Anyway here an article about Lean as a general purpose language https://kirancodes.me/posts/log-ocaml-to-lean.html
> if you're a developer who wants to exploit the multiplicative factor of a truly flexible and extensible programming language with state of the art features from the cutting-edge of PL research, then maybe give Lean a whirl!
Does not sound that appealing to me. Sounds like little consistency and having to learn a new language for every project.
> 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
What I meant is that the part of Idris that lets people prove theorems is the non-total part
But, I think you are right. Haskell could go there by adding a keyword to mark total functions, rather than marking nontotal functions like Idris does. It's otherwise very similar languages
> 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).
Despite what the fanatical constructivists (as opposed to the ones who simply think it's pragmatically nice) seem to want us to think, it turns out that you can prove interesting things with LEM (AKA call/cc) and classical logic.
Yes haskell's
bottombreaks soundness, but that doesn't mean you need to take away some capability from the language. You just need to extend the language with a totality checker for the new proof fragment.OTOH if you really want to emphasize "intended to express proofs" then surely Prolog has that covered, so Lean can be seen as half ML, half Prolog. From this view, the Curry-Howard correspondence is just an implementation detail about choosing a particular computational approach to logic.
Also, basically every such language has escape hatches similar to unsafe in Rust to allow expressions that are not provably terminating.
They can then just be accepted as an axiom.
HTML is not a programming language, it's a markup language - it's in the name, and it's the way it is used (it's not used to describe any kind of computation, it's straight up data that is parsed by algorithms).
Neither is PowerPoint, or game of life a programming language even though both are Turing complete.
https://en.wikipedia.org/wiki/Ladder_logic
Total languages omit partiality and non-termination from Turing completeness.
Partiality is IMO irrelevant when it comes to computability. Any partial function (that is, one whose range is not defined over its whole domain) can be expressed as a total function by either constricting the domain or expanding the range. For example, a "pop" operation on a stack is not defined for an empty stack. You can just loop forever if pop() is called on an empty stack. Alternatively, you can require that pop() is given a witness that the stack is non-empty, or you can require that pop() returns either the top-most element of the stack or a value that indicates the stack was empty. Both let you compute the same set of things as the former.
Non-termination is required to be Turing complete, because being Turing complete means being able to compute functions that one cannot reasonably expect to complete before the heat death of the universe. In _practice_ every function terminates when the computing process dies due to some external factor: process runs out of memory ("real" Turing machines have infinite memory!), user runs out of patience, machine runs out of power, universe runs out of stars, that sort of thing, so _in practice_ doing 2^64 iterations before giving up will generally* give you the same outcome as doing an unbounded number of iterations: it'll either terminate, or the process will be killed (here, due to reaching its iteration limit).
On the flip side, giving up non-termination and partiality only gives you increased correctness. If there's one thing we've definitely established in computing, it's that we will readily discard correctness to gain a little extra productivity. Why make a developer implement code to handle reaching an iteration limit when you can just make the user get sick of waiting and kill your app?
* 18 quintillion is a very large number. Have a try. The most trivial recursive function, on my M4 Mac, when convincing clang to be smart enough to turn it into a loop but dumb enough not to elide it altogether, would take a bit shy of 600 years to complete if iterating ULONG_MAX times; I didn't wait for that, if I'm honest with you, I ran it with a much smaller iteration count and multiplied it out.
Incidentally, this is pretty much what Algol 60 was designed for and why to this day many academic papers use it or a closely related pseudocode.
The results surprised me:
https://github.com/Syzygies/CompareI don't think these results are quite comparable because of slightly differing parallelism strategies; I'd expect the F# implementation of just spinning off threads to be more a little more performant than a Rayon parallel iterator, which presumably has some overhead. But that really just shows how hard it is to do a cross-language comparison; Rust and C++ can certainly be made faster than the F# code by carefully manipulating a ton of low-level OS concurrency primitives. This would arguably also be little misleading. Likewise Chez and Haskell have good C FFI; does that count? It's a tricky and highly qualitative analysis.
[1] FYI, one possible performance improvement with the Chez code is keeping the permutations in fxvectors and replace math operations with the fixnum-specific equivalent - this tells the compiler/interpreter that the data are guaranteed to be machine integers rather than bigints, so they aren't boxed/unboxed. I am not sure without running it myself, but there seems to be avoidable allocations in the Chez implementation. https://cisco.github.io/ChezScheme/csug/objects.html#./objec...
As for parallelism this is a primary concern of mine, and I tried multiple approaches for every language where there was a choice. I used my own work-stealing code only when it beat standard libraries. AI warned me I was in over my head, that writing such a library takes years of experience, but my use case (and my expected use cases in my research) is so uniform that simple can win, minimally touching the required bases such as permuting tasks to avoid false sharing.
I don't believe that the JIT languages (F# on top) do so well because of better parallelism. This is branch optimization. For this use case an AOT compiler with ample benchmark data to influence output should do better. That isn't a thing, and the argument seems to be that few use cases stay consistent. A JIT can adapt.
And BTW I misspoke earlier, of course Chez is AOT rather than JIT. From one approach it's sort of a hybrid: really fast on-the-fly AOT kinda looks like JIT, tongue-in-cheek you could say "NoT compilation" (nick-of-time). But proper JIT of course has huge advantages. If you reeaaaallly wanted to sabotage readability, Chez makes it easy to invoke the compiler at runtime, so along with the C FFI I think you could hack together some sort of JIT. But wow, what a mess that would be! You'd better be getting a PhD thesis out of it :) And if the performance is that critical you'd be much better off with F#.
Given the sane C defaults that are applied by code extraction techniques, the delta really shouldn't be so great. But it's a common pitfall to torture one's own verified code in order to get it proven, and I'm also not sure how good of support there is for parallelism.
Lean 4 is the most interesting language on my list. I didn't reject it on price.
plus up and coming (actual production-ready) languages that don't fit perfectly in the 7 categories: unison, darklang, temporal dataflow, DBSP
It may feel like a little bit of cheating mentioning the above ones, as most are parallel to the regular von Neumann machine setup, but was meaning for a while to do an article with 'all ways we know how to compute (beyond von Neumann)'.
> was meaning for a while to do an article with 'all ways we know how to compute (beyond von Neumann)'.
Would be very glad to read this.
In the meantime, I reproduce a part of an article by Steve Yegge:
---
What Computers Really Are
Another realization I had while reading the book is that just about every course I took in my CS degree was either invented by Johnny von Neumann, or it's building on his work in mostly unintelligent ways.
Where to start? Before von Neumann, the only electronic computing devices were calculators. He invented the modern computer, effectively simulating a Universal Turing Machine because he felt a sequential device would be cheaper and faster to manufacture than a parallel one. I'd say at least 80% of what we learned in our undergrad machine-architecture course was straight out of his first report on designing a programmable computer. It really hasn't changed much.
He created a sequential-instruction device with a fast calculation unit but limited memory and slow data transfer (known as the infamous "von Neumann bottleneck", as if he's somehow responsible for everyone else being too stupid in the past 60 years to come up with something better. In fact, Johnny was well on his way to coming up with a working parallel computer based on neuron-like cellular automata; he probably would have had one in production by 1965 if he hadn't tragically died of cancer in 1957, at age 54.)
Von Neumann knew well the limitations of his sequential computer, but needed to solve real problems with it, so he invented everything you'd need to do so: encoding machine instructions as numbers, fixed-point arithmetic, conditional branching, iteration and program flow control, subroutines, debugging and error checking (both hardware and software), algorithms for converting binary to decimal and back, and mathematical and logical systems for modelling problems so they could be solved (or approximated) on his computing machine.
-Steve Yegge, Math Every Day
https://archive.ph/6tOQF
>term rewriting
In uni we had to make a spreadsheet software.
I volunteered to do the formula parser, thinking it sounded like a fun challenge.
I was stumped for a week, until I realized I could rewrite the formulas into a form I knew how to parse. So it would rewrite 1+1 into ADD(1,1) and so on.
I also refused to learn regex, so the parsing code was "interesting" ;)
I recall a comment from a colleague. "Okay, Andy says it works. Don't touch it." XD
Guy from another group used regex and his solution was 20x shorter than mine.
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.
It made learning Elixir years later much easier.
We also had a course that basically summed up to programming agents to play Unreal Tournament in a language called GOAL which was based on Prolog.
For years I've wanted to use Prolog but could not figure out how. I ended up making a spellcheck to allow LLM's to iterate over and fix the dismal Papiamentu they generate.
I think from a historical perspective, describing COBOL and Fortran as part of the ALGOL family is a stretch, but I suppose it’s a good reminder that all history is reductive.
[0] https://en.wiktionary.org/wiki/cognate
We didn't learn APL (Who is teaching the use of those custom keyboards to 100s of young students for one semester?)
The processing power of systems at the time made it clear which language classes were practically useful and usable for the time and which were not.
Prolog ran like a dog for even simple sets of logic.
We had the best internet access and pretty powerful desktop systems for the time.
I'm still curious why we didn't learn smalltalk. Could have been the difficulty of submitting and marking a system in a particular state rather than a file of code :)
One I might suggest is scripting languages, defined loosely by programming tools which dispatch high-level commands to act on data pipelines: sed, AWK, the sh family, Perl, PowerShell, Python and R as honorary members. In practice I might say SQL belongs here instead of under Prolog, but in theory of course SQL is like Prolog. Bourne shell might be the best representative, even if it's not the oldest.
AWK et al share characteristics from ALGOL and APL, but I feel they are very much their own thing. PowerShell is quite unique among modern languages.
At the same time, I don't agree with that it does not matter if one picks "Java, C#, C++, Python, or Ruby". If your goal is to do quick sort, then well, it does not.
If you want to use language for something (not only for its sake), then it makes a day and night difference. A person who wants to do 3D games and being shown Ruby or a person wanting to do exploratory data science and deep learning and being given Java are likely to get discouraged.
1) Advanced Programming Language Design by Raphael Finkel - A classic (late 90s) book comparing a whole smorgasbord of languages.
2) Design Concepts in Programming Languages by Franklyn Turbak et al. - A comprehensive (and big) book on PL design.
3) Concepts, Techniques and Models of Computer Programming by Peter Van Roy et al. - Shows how to organically add different programming paradigms to a simple core language.
> "What do I mean when I say fundamentals? If you have an array or list of items and you’re going to loop over it, that is the same in any imperative language."
Err
"Fortran: The world’s first programming language standard opened the door to modern computing"
https://www.ibm.com/history/fortran
One thing the article didn’t touch on was SmallTalk’s live visual environment. It’s not a normal source code / text language.
- Forth: you can use PFE,Gforth for ANS Forth requeriments. Or EForth if you reached high skills levels where the missing stuff can be just reimplemented.
EForth under Muxleq: https://github.com/howerj/muxleq I can provide a working config where a 90% of it would be valid across SF.
Starting Forth, ANS version: https://www.forth.com/starting-forth/
Thinking Forth, do this after finishing SF: https://thinking-forth.sourceforge.net/
Also, Forth Scientific Library. You can make it working with both GForth and PFE, just read the docs.
Full pack: https://www.taygeta.com/fsl/library/Library.tgz
Helping Forth code for GForth/PFE. If you put it under scilib/fs-util.fs, load it with:
https://www.taygeta.com/fsl/library/fsl-util.fs- Lisp. s9fes, it will compile under any nix/Mac/BSD out there, even with MinC.
S9fes: http://www.t3x.org/s9fes/
Pick the bleeding edge version, it will compile just fine.
For Windows users: MinC, install both EXE under Windows. First, mincexe, then buildtools*exe: https://minc.commandlinerevolution.nl/english/home.html
Then get 7zip to decompress the s9fes TGZ file, cd to that directory, and run 'make'.
Run ./s9 to get the prompt, or ./s9 file.scm where file.scm it's the source code.
In order to learn Scheme, there's are two newbie recommended books before "SICP".
Pick any, CACS, SS, it doesn't matter, both will guide you before SICP, the 'big' book on Scheme:
Simply Scheme https://people.eecs.berkeley.edu/~bh/pdf/
Simply.scm file, select from ';;; simply.scm version 3.13 (8/11/98)' to '(strings-are-numbers #t)' and save it as simply.scm
https://people.eecs.berkeley.edu/~bh/ssch27/appendix-simply....
Concrete Abstractions
Book:
https://www.d.umn.edu/~tcolburn/cs1581/ConcreteAbstractions....
The SCM files needed to be (load "foo.scm") ed in the code in order to do the exercises:
https://github.com/freezoo/scheme-concabs
If you are en Emacs user, just read the Elisp intro, it will work for a different Lisp family but with similar design.
Spot the differences:
Scheme (like s9):
We try: Elisp/Common Lisp (as the web site shows): Same there: - Ok, ML like languages:https://www.t3x.org/mlite/index.html
If you follow the instructions on compiling s9, mlite it's similar with MinC for Windows. If you are a Unix/Linux/Mac user, you already know how to do that.
You got the whole docs in the TGZ file, and the web.
https://canonical.org/~kragen/memory-models/
jq. there are some antecedents in Icon and xquery, but these generally require explicitly opting into either production or consumption of value streams, where jq does this stream processing automatically from the ground up. (icon requires use of a suspend and needs an every clause to walk the generated values, xquery requires explicit 'for' statements over streams as many builtin operators fail on value streams)in jq, the comma separates expressions, which independently yield values. a span of such expressions is called a 'filter', since they are always run by passing values from the prior filter into them (with the initial values sourcing from json objects on stdin, or an implicit null if you pass -n to the program).
brackets collect values yielded inside of them. if you have a complex object that includes multiple expressions yielding multiple values, construction will permute over them. the pipe operator|runs the next filter with each value yielded by the prior, that value represented by the current value operator.. binding variables in the language is similarly done for each value their source yields functions in the language are neat because you can choose to accept arguments as either early bound values, or as thunks, with the former prefixed with a $.for example, this runs
where this runs. + 100parameters context, with.as the 10,20,30 passed to it:. + 100in the context of its use inside the function, instead receiving 1,2,3: so you could define map taking a current-value array and applying an expression to each entry like so: it's a fun little language for some quick data munging, but the semantics themselves are a decent reason to learn it.for example, I would say what i was taught, that lisp is lists made out of cons cells, which contain references to either other lists/cons cells or to atoms. lisp doesn't "have" parentheses any more than lisp has the rest of the ASCII table, but parentheses were chosen as a convenient way to write list structure down in ascii form because parentheses nest in exactly the way lists do and lists are the important thing.
then there never needs to be another discussion of parentheses and how you feel about them except in a sub-discussion if anybody has any bright ideas about alternative ways to convert list structure to ascii on paper. you disliking parentheses does not mean you dislike lisp; it just means you don't understand lisp, like for instance you think lisp has something to do with ascii.
similar ideas apply to C, wherein the braces and semicolons do not matter, what matters is datatypes that correspond to von neumann architectures including especially pointers, and where binary representation is easily exposed (with a syntax that does not matter but for the record is &, |, ~, ^, <<, or >>. if you hate those choices for operator syntax you could easily convert your own C to use parenthetical lists of CamelCase names of LeftAddRight or whatever floats your boat instead of a + sign), just keep in the front of your mind how data is represented internally and how it's mapped to the syntax you like, and whatever list structure you choose to order the lines of code)
Ur-ness is not interesting, just as the city of Ur was no doubt a lot less interesting than the city of Rome. Study Algol only to learn about call-by-name, then forget it.
I could go on, but, like the ripples from a gold coin thrown in the bay, the effect will soon dissipate as if I had never written anything at all.