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

On Sun, 2008-01-06 at 16:19 +0100, Daniel Fischer wrote:

Am Sonntag, 6. Januar 2008 15:54 schrieb Achim Schneider:

...

Daniel Fischer wrote:

...

Am Sonntag, 6. Januar 2008 15:18 schrieb Andrew Coppin:

...

Daniel Fischer wrote:

...

Just because I don't know: what bugs would be possible in a language having only the instruction return ()

Bug #1: You cannot write any nontrivial programs. ;-)

That's not a bug, that's a feature.

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.

I'm not a logician, but didn't Gödel prove that you couldn't express the (full) arithmetic of natural numbers in such a language? Of course it might be possible to express a sufficiently interesting part of it, but I should be surprised.

What Goedel meant by "arithmetic" is a bit more than one usually associates with the term. One person mentioned Epigram. Most theorem provers and most? (of the few) dependently typed programming languages would fit Achim's criterion depending on the range of "usable" and "usual". Coq, for example, is likely to be capable of formalizing just about anything you'd want. Of course, there is one class of "programming problem" that we can already say can't be handled; namely implementing interpreters (for Turing complete languages). We can formalize analyses, make compilers, prove the compilers correct with respect to a semantics, and even prove that a -description- of an interpreter correctly implements the semantics, but we can't actually -run- the interpreter.