Comment by pjmlp

> 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...

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