Lambda the Ultimate

I've noticed the beginning of a trend in hobbyist/amateur programming language theory. There have been a number of recent programming languages that have extremely minimalistic semantics, to the point of being anemic. These languages typically define function types, product types, the unit type, perhaps natural numbers, and not much else. These languages are typically capable of universal computation, but executing programs in them directly would be comically slow, and so what they do is recognize special strings of code and replace them with implementations written in a faster meta-language. This pair of the recognized string of code and the efficient replacement is known as a "jet", or an "accelerator".

Some languages that do this:

• Urbit's Nock, which, other than the jet concept, I honestly think is either a strange art project or snake oil, so I won't discuss this further.
• Simplicity, a smart contract language for blockchain programming by Blockstream.
• David Barbour's Awelon, which is the most minimalistic of all three of these by only defining function types!

My question is this: is this idea of "jets" or "accelerators" a serious approach to programming language implementation? There's an obvious question that comes to mind: how do you know the object language program and the meta-language program you've replaced it with are equivalent? Simplicity claims to have done a number of Coq proofs of equivalence, but I can't imagine that being sustainable given the difficulty of theorem proving and the small number of developers able to write such a proof. Urbit takes a rather cavalier attitude towards jet equivalence by advocating testing and simply treating the jet as the ground truth in the case of a conflict. And I know David posts here so I hope he will respond with Awelon's take on this matter.

Here is an excerpt from the Simplicity document arguing in favor of jets:

• Jets provide a formal specification of their behavior. The implementation
of a jet must produce output identical to the output that would be pro-
duced by the Simplicity expression being replaced. There is no possibility
for an ambiguous interpretation of what a jet computes.
• Jets cannot accidentally introduce new behavior or new side effects be-
cause they can only replicate the behavior of Simplicity expressions. To
add new behavior to Simplicity we must explicitly extend Simplicity (see
Section 4).
• Jets are transparent when it comes to reasoning about Simplicity expres-
sions. Jets are logically equal to the code they replace. Therefore, when
proving properties of one’s Simplicity code, jets can safely be ignored.

Naturally, we expect jetted expressions to have properties already proven and available; this will aid reasoning about Simplicity programs that make use of jets.

Because jets are transparent, the static analyses of resource costs are not affected by their existence. To encourage the use of jets, we anticipate discounts to be applied to the resource costs of programs that use jets based on the estimated savings of using jets.

When a suitably rich set of jets is available, we expect the bulk of the
computation specified by a Simplicity program to be made up of these jets, with only a few combinators used to combine the various jets. This should bring the computational requirements needed for Simplicity programs in line with existing blockchain languages. In light of this, one could consider Simplicity to be a family of languages, where each language is defined by a set of jets that provide computational elements tailored for its particular application.

In the interest of charity, I'll also try to make an argument in favor of this approach, although I remain skeptical: an extremely minimal programming language semantics means a language designer can truly consider their work to be done at some point, with no further room for improvement. A minimalistic Python would have largely avoided the fiasco involved in the upgrade from Python 2 to Python 3, by pushing all of the breaking changes to the library level, and allowing for more gradual adoption. Languages features added to JavaScript in recent years (like classes, async/await, modules and so on) would also have been libraries and presentation layer additions instead of breaking changes at the implementation level.