[Haskell-cafe] Why isn't "Program Derivation" a first class citizen?

[Jon Fairbairn]

Rustom Mody <rustompmody at gmail.com> writes:

> On Wed, Feb 13, 2013 at 4:17 AM, Nehal Patel <nehal.alum at 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.Fairbairn at cl.cam.ac.uk