[Haskell-cafe] Proof that Haskell is RT
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:
>> 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
More information about the Haskell-Cafe