On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean
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