[Haskell-cafe] Re: Re: US Homeland Security program language security risks

[Ben Franksen]

Miguel Mitrofanov wrote:
>> That's an interesting task: Design a non-touring complete,
>> restricted language in which every expression is decidable, without
>> making the language unusable for usual programming problems.
> 
> Well, I did something like that a few years ago - it was a sort of
> assembler language, allowing the programmer to, say, sort an array,
> but not to calculate Akkerman function.

P. Wadler, in his famous paper "Theorems for free!", writes on page
2: "Indeed, every recursive function that can be proved total in second
order Peano arithmetic can be written as a term in the Girard/Reynolds
calculus [...]. This includes, for instancs, Ackerman's function [...], but
excludes interpreters for most languages (including the Girard/Reynolds
calculus itself)." BTW, another name for the Girard/Reynolds calculus
is "(pure) polymorphic lambda calculus"; and yes, it is strongly
normalizing. (Wadler cites some papers to support the above claim.)

It seems there is quite a lot of interesting stuff that can be done in a
language where every expression is guaranteed to terminate.

Cheers
Ben