Rustom Mody <rustompm...@gmail.com> writes: > On Wed, Feb 13, 2013 at 4:17 AM, Nehal Patel <nehal.a...@gmail.com> wrote: >> ---- >> Why isn't "Program Derivation" a first class citizen? >> --- > I am stating these things from somewhat foggy memory (dont have any > lambda-calculus texts handy) and so will welcome corrections from those who > know better… > > In lambda-calculus, if reduction means beta-reduction, then equality is
semi > decidable > If a theorem-prover were as 'hands-free' as a programming language > Or if an implemented programming language could do the proving that a > theorem-prover could do, it would contradict the halting-problem/Rice > theorem. Just so, but I’ve long (I suggested something of the sort to a PhD student in about 1991 but he wasn’t interested) thought that, since automatic programme transformation isn’t going to work (for the reason you give), having manually written programme tranformations as part of the code would be a useful way of coding. RULES pragmas go a little way towards this, but the idea would be that the language supply various known valid transformation operators (akin to theorem proving such as in HOL), and programmers would explicitly write transformation for their functions that the compiler would apply. -- Jón Fairbairn jon.fairba...@cl.cam.ac.uk _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe