Tail pad optimization, cache friendlyness and C++ interrop

[Timon Gehr via Digitalmars-d]

On 06/19/2014 09:06 PM, "Ola Fosheim Grøstad" 
<ola.fosheim.grostad+dlang at gmail.com>" wrote:
> On Thursday, 19 June 2014 at 18:25:00 UTC, Tobias Pankrath wrote:
>> It's not. Since the resources to verify a property are limited, too.
>>
>> If I need to enumerate all possible program states, there will always
>> exists a program that can run on my box but will not be verifiable on
>> it (since I lack the resources).
>
> Nobody have said you should enumerate all possible states.
>
> There's a significant difference between a proof and an algorithm.

I don't think it is that significant. They are basically the same except 
that the proof is typically more strongly typed and you cannot actually 
execute a proof by excluded middle in the general case.