Re: RA with MV attributes

"Marshall" <marshall.spight_at_gmail.com> wrote:

>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.

     Thank you. I was concerned that you were not seeing this, and it is important (at least to me).

>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.

     Truly.

>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.

     I think it is possible.

     If I want something quick and dirty, I need not do anything to my code. I compile with "accept everything".

     If I want severe checking, then I set flags appropriately and possibly have to add to my code to indicate special treatment.

Sincerely,

Gene Wirchenko

Computerese Irregular Verb Conjugation:

     I have preferences.
     You have biases.
     He/She has prejudices.