OT (partially): about promotion of integers

[Timon Gehr]

On 12/13/2012 12:43 AM, Walter Bright wrote:
> On 12/12/2012 3:23 PM, Timon Gehr wrote:
>> It is somewhat similar to (the still quite broken) 'pure' in D,
>
> Broken how?
>

- There is no way to specify that a delegate is strongly pure without 
resorting to type deduction, because
   - Member functions/local functions are handled inconsistently.
     - Delegate types legally obtained from certain member functions are 
illegal to declare.
     - 'pure' means 'weakly pure' for member functions and 'strongly 
pure' for local functions. Therefore it means 'weakly pure' for 
delegates, as those can be obtained from both.
- Delegates may break the transitivity of immutable, and by extension, 
shared.

A good first step in fixing up immutable/shared would be to make 
everything that is annotated 'error' pass, and the line annotated 'ok' 
should fail:

import std.stdio;

struct S{
	int x;
	int foo()pure{
		return x++;
	}
	int bar()immutable pure{
		// return x++; // error
		return 2;
	}
}

int delegate()pure s(){
	int x;
	int foo()pure{
		// return x++; // error
		return 2;
	}
	/+int bar()immutable pure{ // error
		return 2;
	}+/
	return &foo;
}

void main(){
	S s;
	int delegate()pure dg = &s.foo;
	// int delegate()pure immutable dg2 = &s.bar; // error
	writeln(dg(), dg(), dg(), dg()); // 0123
	immutable int delegate()pure dg3 = dg; // ok
	writeln(dg3(), dg3(), dg3(), dg3()); // 4567
	// static assert(is(typeof(cast()dg3)==int delegate() immutable pure)); 
// error
	auto bar = &s.bar;
	pragma(msg, typeof(bar)); // "int delegate() immutable pure"
}


>> Provided the code is correct.
>
> No language or compiler can prove code correct.

Sometimes it can. Certainly a compiler can check a user-provided proof.
eg: http://coq.inria.fr/

A minor issue with proving code correct is of course that the proven 
specification might contain an error. The formal specification is often 
far more explicit and easier to verify manually than the program though.