checkedint call removal

Timon Gehr via Digitalmars-d digitalmars-d at puremagic.com
Wed Jul 30 08:24:56 PDT 2014


On 07/30/2014 09:22 AM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= 
<ola.fosheim.grostad+dlang at gmail.com>" wrote:
> On Tuesday, 29 July 2014 at 22:07:42 UTC, Timon Gehr wrote:
>> On 07/29/2014 11:08 PM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?=
>> <ola.fosheim.grostad+dlang at gmail.com>" wrote:
>>> The best you can hope to have is partial correctness. Even with a system
>>> for formal verification.
>>
>> Well, why would this be true?
>
> Because there is no way you can prove say OpenGL drivers to be correct.
> They are a black box provided by the execution environment.

I see. (Though I secretly still dare to hope for verified OpenGL 
drivers, or something analogous: it is not completely out of reach 
theoretically; the machine can be given a quite precise formal 
specification.)

Note that 'partial correctness' usually means that the program runs 
correctly conditional on its termination, hence my confusion.


More information about the Digitalmars-d mailing list