[Haskell-cafe] Strong Normalization was Re: W3C discussion: Principle of Least Power

[Shae Matijs Erisson]

Graham Klyne <GK at ninebynine.org> writes:

> Can it truly be said that it's easier to analyze a functional expression than
> a C program?  What could that actually mean?  I feel the discussion is (so
> far) missing a trick, but I'm not sure what it is.

The LtU article "What good is strong normalization in programming
languages?"[1] may be helpful here. Barry Jay's comment about always
terminating data access plus loops or fixpoints interests me in particular.

I wonder, would it be useful to have a language designed entirely that way?
Could you have a terminating language with only a single top level loop?
Could any two programs be composed such that the result still only has a single
top level loop? Would a language structured that way be advantageous for
debugging, proof assistants, or other verifications?

[1] http://lambda-the-ultimate.org/node/view/1120
--
Shae Matijs Erisson - http://www.ScannedInAvian.com/ - Sockmonster once said:
You could switch out the unicycles for badgers, and the game would be the same.