Reading Raph’s post, it occurs to me that the fact that it’s harder to make GUIs in Rust could be a signal that GUIs in general are harder to prove correct than other programs. Or at least, with the approaches that are common today.
No, it only signals that GUIs are hard to write given Rust's constraints. Ralph's post reiterates something already well known -- Rust sharply limits the kinds of designs that can be implemented in it ... and that's not a good feature of a systems programming language. Again, language design should not be based on throwing up road blocks.
While Rust prevents certain classes of error, in no way are Rust programs provably correct. Your program may not have dangling pointers or cross-thread race conditions, but it can certainly panic, infinitely loop, deadlock, or give wrong results. And there are other memory-safe languages, notably those with garbage collection ... Rust found a clever way to achieve memory safety without garbage collection (and relatedly, without putting nearly everything on the heap, as "managed" VM systems do), but it pays a heavy price for it. There are projects where the trade off Rust offers is highly desirable, and what Rust offers is unique and valuable, but such projects are relatively scarce and GUIs aren't among them.
That said, future versions of Rust may open up the design space some ... the mention here of ways to delegate method calls to a struct member, for instance (however, looking at Looking at Efficient code reuse · Issue #349 · rust-lang/rfcs · GitHub, I suspect that it will be a very long time before it comes to Rust). This is important in a language that not only has a preference for composition over inheritance, but demands it. D has such forwarding as well as other features that reduce the friction in such designs, as well as numerous other designs. (Its one big limitation is the lack of a gc-free core library -- you can code in D without gc, but you lose strings and other important features. It's too bad D doesn't have any corporate backing. Nim is another systems programming language that has a lot of technical merit but is developed on a shoe string.)