Memory allocation purity

[Andrei Alexandrescu via Digitalmars-d]

On 5/16/14, 4:53 AM, Timon Gehr wrote:
> 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

Typo: int_leibiz_equality :o). -- Andrei