On 07/30/2014 09:22 AM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?=
<[email protected]>" 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?=
<[email protected]>" 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.
