"To solve that emacs needs to be divorced from unexec, something that needs to get done as the marriage is unhealthy, but it’s going to take a lot to make that a reality right now."
unexec perspectives from the Remacs gitter room
miniblog.
Related Posts
Formal Verification: The Gap Between Perfect Code and Reality https://raywang.tech/2017/12/20/Formal-Verification:-The-Gap-between-Perfect-Code-and-Reality/
Good critique of how formal verification techniques can be extremely heavyweight. Also discusses (rather pessimistically) how it's important to know which parts are not verified
Not all feasible technology will be built. It takes a strong advocate and big engineering push to bring it to reality. Thoughts from Bill Joy in

