Bruno Oliveira wrote: > Hi Frank! > > But then I have a paradox ...
>>>Clearly a misconception of mine. >
Frank: >>I'm afraid the misconception is Conor's.
Frank, does it make sense to you to call a logical system `sound' if you can use it to prove things which aren't true?
I did seek to be clear that I was interpreting `soundness' as consistency, which seemed to be the appropriate notion when considering the Curry-Howard correspondence. My mistake.
Haskell is not a `logical system' (why not?), so perhaps you can call it `sound' with weaker justification, such as
>>Haskell's type system is (so far as we know) sound: this means programs >>will not crash.
This, I referred to as `type safety'. I happen to think that such a weak notion doesn't deserve the designation `soundness', but it seems that this is a misconception. Fair enough. It feels good to be sound, doesn't it?
Bruno:
> Well, the other possibility is, there are two different meanings for soundness :)
Only two? If we redesignate segmentation-fault-core-dumped a `value', perhaps we can convince ourselves that C's type system is `sound'. Such a scenario would provide even greater scope for violent agreement than we currently enjoy.
But perhaps, in the interests of avoiding further misconception, we had better follow the Duchess's dictum:
Take care of the sense, and the sounds will take care of themselves.
Cheers
Conor _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
