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

[Derek Elkins]

On Sun, 2008-01-06 at 16:19 +0100, Daniel Fischer wrote:
> Am Sonntag, 6. Januar 2008 15:54 schrieb Achim Schneider:
> > Daniel Fischer <daniel.is.fischer at web.de> 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.