Memory allocation purity

[Timon Gehr via Digitalmars-d]

On 05/16/2014 01:00 AM, H. S. Teoh via Digitalmars-d wrote:
> On Thu, May 15, 2014 at 03:22:25PM -0700, Walter Bright via Digitalmars-d wrote:
>> On 5/15/2014 2:41 PM, Timon Gehr wrote:
>>> On 05/15/2014 11:33 PM, Walter Bright wrote:
>>>> On 5/15/2014 9:07 AM, Timon Gehr wrote:
>>>>> Why? A memoizable function is still memoizable if it is changed
>>>>> internally to memoize values in global memory, for example.
>>>>
>>>> I doubt a compiler could prove it was pure.
>>>>
>>>
>>> Yes, that was actually my point. Memoizable is actually a non-trivial
>>> property.
>>>
>>> (But note that while a compiler cannot in general discover a proof,
>>> it could just _check_ a supplied proof.)
>>
>> If the compiler cannot mechanically verify purity, the notion of
>> purity is rather useless, since as this thread shows it is incredibly
>> easy for humans to be mistaken about it.
>
> What if the language allowed the user to supply a proof of purity, which
> can be mechanically checked?
>
> Just rephrasing what Timon said, though -- I've no idea how such a thing
> might be implemented. You'd need some kind of metalanguage for writing
> the proof in, perhaps inside a proof block attached to the function
> declaration, that can be mechanically verified to be correct.

Yes, either that or one could even just implement it in the existing 
language by introducing types for evidence, and basic termination checking.

eg. http://dpaste.dzfl.pl/33018edab028
(This is a really basic example. Templates or more language features 
could be used to simplify some of the more tedious steps, but I think it 
illustrates well the basic ideas. Maybe there are some small mistakes 
because I didn't find the time to actually implement the checker.)


> Alternatively, if only one or two statements are causing trouble, the
> proof can provide mechanically checkable evidence just for those
> specific statements.
>
> The metalanguage must be mechanically checkable, of course. But this may
> be more plausible than it sounds -- for example, solutions to certain
> NP-complete problems are verifiable within a far shorter time than it
> would take to actually solve said problem.

Indeed checking whether there is a proof of some fact up to some 
specific length N for a powerful enough logic is an NP-complete problem. 
(If N is encoded in unary.)

> This suggests that perhaps,
> while the purity of an arbitrary piece of code is, in general,
> infeasible for the compiler to mechanically prove, it may be possible in
> some cases that the compiler can mechanically verify a user-supplied
> proof, and thus provide the same guarantees as it would for
> directly-provable code.
>
>
> T
>

In fact, this would cover most cases. Usually there is some checkable 
reason why a piece of code is correct (because otherwise it would not 
have been invented in the first place.)