[Haskell-cafe] Proof that Haskell is RT

[Luke Palmer]

On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean <jules at jellybean.co.uk> wrote:
> Andrew Birkett wrote:
>>
>> Hi,
>>
>> Is a formal proof that the Haskell language is referentially transparent?
>>  Many people state "haskell is RT" without backing up that claim.  I know
>> that, in practice, I can't write any counter-examples but that's a bit
>> handy-wavy.  Is there a formal proof that, for all possible haskell
>> programs, we can replace coreferent expressions without changing the meaning
>> of a program?
>
> The (well, a natural approach to a) formal proof would be to give a formal
> semantics for haskell.

Haskell 98 does not seem that big to me (it's not teeny, but it's
nothing like C++), yet we are continually embarrassed about not having
any formal semantics.  What are the challenges preventing its
creation?

Luke