[bpavuk]

ffmpeg is actually asm and for a good reason - it has to go fucking fast or else media playback will take too much resources

[dblohm7]

There are projects such as Halide[1] that actually allow you to achieve performance without needing to resort to asm.

[1] https://halide-lang.org/

[inigyou]

Great then let's prove that ASM is correct.

the reference C code is just as bad.

[pjmlp]

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]

It's smallish snippets that implement self-contained algorithms, which should make it well within reach of direct formal proof of correctness.