3 ms·
Formally verifying your window manager sounds like the ultimate yak shaving experience.
by laretluval 10y ago
Formally verifying your window manager sounds like the ultimate yak shaving experience.
- wtallis 10y agoThe 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.
- xupybd 10y agoTrue, 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.
- nickpsecurity 10y agoIf 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.