13 Feb
2009
13 Feb
'09
2:21 p.m.
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