See also the XMonad module X.A.Navigation2D which includes formal proofs of the navigational strategies:

PDF: https://web.cs.dal.ca/~nzeh/xmonad/Navigation2D.pdf

Module: https://hackage.haskell.org/package/xmonad-contrib-0.13/docs...

Formally verifying your window manager sounds like the ultimate yak shaving experience.

The point of this exercise wasn't really to have a formally verified window manager, it was to document what it's like to make formally verified software. As a modestly complex program and one of the most well-known Haskell programs, xmonad was a good choice.

And while I agree that a formally verified X window manager seems a bit silly, a formally verified Wayland compositor would be a great idea given their broad scope of responsibilities.

True, but the number of times I have to restart because Gnome has borked and is no longer recognising mouse clicks, makes me think it has a place.

If you do it right, you only need to verify a few key components with interface conditions on how the rest should use them. This approach was taken in high-assurance security to build window managers that prevented leaks between apps or login spoofing. Nitpicker GUI is a modern example of that at least architecturally.

I feel like Idris would have a better experience for problems like this, quite excited about it right now.