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.
