Re: RA with MV attributes

On Jan 18, 10:13 am, Gene Wirchenko <g..._at_ocis.net> wrote:
> "Marshall" <marshall.spi..._at_gmail.com> wrote:
>
> >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.

> That will come at the cost of possibly throwing out a program
> that works, but that the proof system can not prove as working.

Yes, absolutely. Which for some applications (not many) is not merely worth it but mandatory. There is software that lives depend on.

On the other hand, there are software systems where they don't even want to be bothered with a compile step. "The compiler just gets in my way" they say. These two represent the endpoints in a continuum.

Right now we have disparate systems that satisfy both groups. But those systems don't look anything like each other, and their position on the correctness-proof continuum is fixed. The question is, can we accomodate both types of users in a single system? I think it's possible, or at least approachable. Or at the very very least, an interesting question to think about.

Marshall Received on Thu Jan 18 2007 - 21:54:57 CET