Memory allocation purity

[H. S. Teoh via Digitalmars-d]

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.
Alternatively, if only one or two statements are causing trouble, the
proof can provide mechanically checkable evidence just for those
specific statements.

The metalanguage must be mechanically checkable, of course. But this may
be more plausible than it sounds -- for example, solutions to certain
NP-complete problems are verifiable within a far shorter time than it
would take to actually solve said problem. This suggests that perhaps,
while the purity of an arbitrary piece of code is, in general,
infeasible for the compiler to mechanically prove, 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.


T

-- 
When solving a problem, take care that you do not become part of the problem.