Memory allocation purity

[bearophile via Digitalmars-d]

H. S. Teoh:

> 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.

Yes, this is common enough. As an example the Whiley 
(http://whiley.org/ ) is not able to find the proof for various 
invariants and contracts, but the programmer can write them down 
and Whiley verifies them to be correct during the compilation. 
Inventing a proof is harder, but verifying it is often much 
easier.

The first way D can introduce such things (simple proof) is in 
the static verify of some contracts.

Verifying @memoizable or @reflexive/@symmetric/@transitive (for 
functions with two arguments) is perhaps a bit too much ambitious 
for D compilers. But it surely goes well with the idea of a 
language that tries to both avoid bugs and generate efficient 
binaries :-) (And perhaps someday C++ Axioms of Concepts will be 
handled by a C++ compiler able to verify a function to be 
symmetric).

Bye,
bearophile