Re: RA with MV attributes

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

>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

                                                                  ^^^^
     Magic Weasel Word!

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

     The magic weasel word is "some". You can also write some code that will correctly recognise whether some pieces of code will ever, say, generate an integer overflow.

     If you can not tell if said program will ever terminate, it will not be possible, in general, to tell if it will ever generate an integer overflow.

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

Sincerely,

Gene Wirchenko

Computerese Irregular Verb Conjugation:

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