Memory allocation purity

[Steven Schveighoffer via Digitalmars-d]

On Mon, 19 May 2014 16:56:58 -0400, Ola Fosheim Grøstad  
<ola.fosheim.grostad+dlang at gmail.com> wrote:

> On Monday, 19 May 2014 at 18:55:57 UTC, Steven Schveighoffer wrote:
>> On Mon, 19 May 2014 14:49:41 -0400, Ola Fosheim Grøstad  
>> <ola.fosheim.grostad+dlang at gmail.com> wrote:
>>
>>> On Monday, 19 May 2014 at 18:33:55 UTC, Steven Schveighoffer wrote:
>>
>>>> Then you should have no problem producing an example, right?
>>>
>>> I did. Besides, I think language constructs should be proven sound a  
>>> priori, not post mortem...
>>
>> Let me cut to the chase here. I haven't seen it. Let's not go any  
>> further until you can produce it.
>
> I've given several examples

Links?

> , but I oppose the general attitude. Language constructs should be  
> formally proven correct. Proving a program to be correct is usually not  
> worth it, but for individual language construct it is indeed possible  
> and necessary, optimization depends on it.

I think it is correct. How is it not? Proving correct is very difficult,  
proving incorrect is not difficult. Just a counter example is needed. So  
far, the examples have not disproven the point.

> If optimization change semantics you will risk efficient algorithm  
> implementations either going wrong or into an infinite loop. Not at all  
> suitable for a programming language that aims for system level  
> efficiency and generic programming.

It's not incorrect, just a bug to depend on an allocator allocating two  
different addresses, or allocating in a certain order.

In other words, inside a pure function, an allocator of an immutable  
object is to be treated as if it may or may not choose to return the same  
object. That's just what you should expect. Expecting something else is a  
BUG.

-Steve