← Back to context Comment by inigyou 2 days ago Great then let's prove that ASM is correct.the reference C code is just as bad. 2 comments inigyou Reply 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. inigyou 2 days ago It's smallish snippets that implement self-contained algorithms, which should make it well within reach of direct formal proof of correctness.
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. inigyou 2 days ago It's smallish snippets that implement self-contained algorithms, which should make it well within reach of direct formal proof of correctness.
inigyou 2 days ago It's smallish snippets that implement self-contained algorithms, which should make it well within reach of direct formal proof of correctness.
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.