I think a lot of that is just the poverty of UI APIs and especially the imperative drawing paradigm. There's no reason in principle why we can't programmatically verify that the basics of the UI spec are fulfilled. If the whole UI layer is just impossible to verify then if we're at all serious about correctness then we should (hyperbolically) stop making UIs until we figure it out.
