Article about xmonad not making X errors?
I recall reading at some point an article or blog post that discussed how XMonad leveraged the type system to guarantee that X errors couldn't occur. But no matter how much googling I do now I can't find it; I musn't be using the right search terms. Anyone know where it is?
Joseph Garvin wrote:
I recall reading at some point an article or blog post that discussed how XMonad leveraged the type system to guarantee that X errors couldn't occur. But no matter how much googling I do now I can't find it; I musn't be using the right search terms. Anyone know where it is?
The type system can't guarantee that xmonad produces no X errors, since it relies on the ffi and secondly, matching types don't imply correctness, especially when dealing with IO-ish stuff. I think you might be referring to this article by Neil Mitchell(author of Hoogle and Catch, iirc) that proves for an old xmonad that the core won't fail due to error-calls or failed pattern matches: http://neilmitchell.blogspot.com/2007/05/does-xmonad-crash.html
asgaroth_:
Joseph Garvin wrote:
I recall reading at some point an article or blog post that discussed how XMonad leveraged the type system to guarantee that X errors couldn't occur. But no matter how much googling I do now I can't find it; I musn't be using the right search terms. Anyone know where it is?
The type system can't guarantee that xmonad produces no X errors, since it relies on the ffi and secondly, matching types don't imply correctness, especially when dealing with IO-ish stuff. I think you
We do use the type system for a number of invariants, though. But by no means can we guarantee *no* errors -- we'd need a specification of the X server in a theorem prover to even start... :) -- Don
participants (3)
-
Daniel Schoepe -
Don Stewart -
Joseph Garvin