On 05/16/2014 01:00 AM, H. S. Teoh via Digitalmars-d wrote:
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.
Yes, either that or one could even just implement it in the existing
language by introducing types for evidence, and basic termination checking.
eg. http://dpaste.dzfl.pl/33018edab028
(This is a really basic example. Templates or more language features
could be used to simplify some of the more tedious steps, but I think it
illustrates well the basic ideas. Maybe there are some small mistakes
because I didn't find the time to actually implement the checker.)
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.
Indeed checking whether there is a proof of some fact up to some
specific length N for a powerful enough logic is an NP-complete problem.
(If N is encoded in unary.)
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
In fact, this would cover most cases. Usually there is some checkable
reason why a piece of code is correct (because otherwise it would not
have been invented in the first place.)
