Re: RA with MV attributes

On Jan 17, 10:32 pm, Gene Wirchenko <g..._at_ocis.net> wrote:
> "Marshall" <marshall.spi..._at_gmail.com> wrote:
>
> >> Like VB 6? You can declare variables as being of one type (say,
> >> Integer) or any (Variant).
>
> >Sure, that's a start. However what I'm starting to imagine is something
> >that AFAIK is not in any existent language. The idea is that a given
> >module could be capable of very strict static checking, such as proving
> >the absence of infinite loops, faults such as divide by zero, and
> >freedom
> >from stack overflows through a proof of maximum resource usage.
> >Another module could be completely free from such requirements,
> >fully dynamic, having all checking deferred until runtime. All in the
> >same language; the choice of where in the continuum you are made
> >by the programmer based on the needs of the current application.
>
> I think that a general solution would require a solution to the
> halting problem.

No, no, I'm not proposing writing a program that tells whether another program halts or not; that is of course impossible. However it is certainly possible to write code that can correctly recognize some programs as halting, some programs as diverging, and for other programs it cannot tell. There are certain classes of applications for which a proof of termination is highly desirable, and some of the people building these systems already use termination proofs.

If one were writing such an application, which has such very strict requirements, one might well want a language that will issue a compile error unless it has a termination proof of the program, whether it is human supplied or automatically generated, or a mix.

Marshall Received on Thu Jan 18 2007 - 08:51:05 CET