Memory allocation purity

[via Digitalmars-d]

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, 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. This is also why you should strive 
for a small set of primitives and build high level constructs by 
lowering them to the minimal language. You can then limit your 
proof to the primitives.

The basic idea in generic programming is that you can implement 
the full blown generic algorithm, plug in the parts that can vary 
and let the optimizing compiler boil it down into an optimized 
tight machine language construct. The programmer should not be 
required to "deduce" what will happen when he plugs stuff into 
the generic algorithm.

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.