Comment by bpavuk
3 days ago
ffmpeg is actually asm and for a good reason - it has to go fucking fast or else media playback will take too much resources
3 days ago
ffmpeg is actually asm and for a good reason - it has to go fucking fast or else media playback will take too much resources
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/
Great then let's prove that ASM is correct.
the reference C code is just as bad.
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.