[Haskell-cafe] Proof that Haskell is RT
Luke Palmer
lrpalmer at gmail.com
Wed Nov 12 07:39:10 EST 2008
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
More information about the Haskell-Cafe
mailing list