> Aside: verified assembly This isn't new, it is actually part of how Dafny came to be, another formal verification programming language. "Safe to the Last In

> Aside: verified assembly This isn't new, it is actually part of how Dafny came to be, another formal verification programming language. "Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System" https://www.microsoft.com/en-us/research/publication/safe-to-the-last-instruction-automated-verification-of-a-type-safe-operating-system https://www.microsoft.com/en-us/research/publication/safe-to... However so far hardly anyone in mainstram cared about verified assembly, maybe now with LLMs. "Programming Language Design and Implementation in the Era of Machine Learning" https://www.youtube.com/watch?v=Fc3cW0nqAQ0 https://www.youtube.com/watch?v=Fc3cW0nqAQ0