Comment by pjmlp
2 days ago
Which is actually possible, unfortunately the industry never cared that much about strong typed assembly.
See Verve OS from Microsoft Research, TAL and the origins of the Dafny language.
2 days ago
Which is actually possible, unfortunately the industry never cared that much about strong typed assembly.
See Verve OS from Microsoft Research, TAL and the origins of the Dafny language.
It's smallish snippets that implement self-contained algorithms, which should make it well within reach of direct formal proof of correctness.