Hi 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