world as value

[Erik Zuurbier]

>Hi everybody,
>
>I want to start a discussion about Clean's "world as value" paradigm.

[snip]

>best wishes
>  Martin Wierich
>  University of Nijmegen

I read this account top to bottom, so I only read that it was posted by Martin
at the end. That scared me a bit. If anybody should know about these
problems, the Nijmegen boys should. I always assumed that there would be
something I only partly understood, relying on formal proofs made, checked
and double checked by the academics. Wrongly, I guess. But CAN I assume
that you have talked to theorists such as Sjaak Smetsers and Peter Achten
about this?

One thing I know is that some programs are inherently non-deterministic,
such as airline reservation systems where the success of one passenger's
booking depends on cumulative other bookings up to the moment (s)he calls.
I also learned to accept (rather than profoundly understand) that with
Peter Achten's IO-system you could model that, and at the same time claim
that the system remained 'pure and functional' in the sense that all
continues to be referentially transparent.

Are you claiming that Peter's system is shaky? That it is lacking a proper
proof? Have I missed theoretical articles that have already uncovered the
questionable fundamentals of the 'world as value' paradigm long ago
(probably by Haskell theorists)?

Or are you seeking a semantics that only covers deterministic programs?

Regards Erik Zuurbier