Lambda the Ultimate

There is Statically Allocated Parallel Functional Language (SAFL) by Mycroft and Sharp that also enforces this style:

• All allocations are static.
• All loopy code is tail call optimized.

It doesn't quite guarantee progress (i.e. a loop could diverge), though it probably could with some extra analysis.

Also, while not yet suitable for 'performance' concerns...

I've developed a simple functional bytecode, ABC, that lacks any jumps, neither forward nor backward. Bytecode is evaluated in one direction. But ABC can represent first class functions - a finite 'block' of code. Conditional behavior is expressed by conditional application of a block, and loopy code via a simple fixpoint combinator.

ABC was developed to support streamable code, ability to express applications (and full virtual environments) as append-only logs, and easily share and distribute both behavior and data. Performance wasn't a primary concern, though I have strategies that should make it competitive long term.

Bitcoin supports a scripting language that allows coins to be spent only when a script runs and produces a positive result. The usual script just checks that the transaction spending it is signed with a private key that matches the public-key signature on the coins.

Satoshi Nakamoto (designer of Bitcoin) initially had a forth-ish stack language for the scripting. Hal Finney demonstrated several attacks that would be enabled by subroutines and/or back branching - they ranged from locking problems and race conditions to excessive resource consumption of CPU, bandwidth, and/or memory. Bitcoin went live with all back branch and subroutine enabling instructions removed from the scripting language. So there can be jumps forward (sections of code can be skipped) but no jumps backward. Every subsequent instruction in serialization order is also a subsequent instruction in execution order.

This is a pretty common compilation strategy for synchronous dataflow languages. The mathematical idea is that you can represent an arbitrary stream transducer f : Stream(Input) -> Stream(Output) as a state machine, with an initial state s : S and a transition function step : S * Input -> S * Output.

So the generated code for f has a single while loop, which waits for inputs, and runs the body of the loop implementing the step function to incrementally produce outputs. Marc Pouzet has some slides describing how this works here.

Purely of historical interest, the first paper of which I'm aware which touches on this issue is from just over half a century* ago:

Corrado Böhm et Guiseppe Jacopini, « Flow diagrams, Turing Machines and Languages with only Two Formation Rules », CACM v9n5, 1966

(* early enough that it's written in the language of flowcharts, and I have difficulty following the arguments. WP suggests that the "single while loop" is a folk version of their result, and probably predates it, going back to [computer] antiquity)

_{other contents of the same issue, a pair which may have aged more gracefully: « a note on "program structures for parallel processing" » and « Additionally comments on a problem in concurrent program control » and one which probably is also now purely of historical interest: « 11/16" perforated paper tape ».}