> If you had good tooling, you could annotate the assembly routine as being equivalent to the C implementation; then maintenance would be a lot easier, since the compiler would yell at you if they ever diverged.

Is that something actual compilers can do right now? I don't think I have heard of something like though, though I don't work that close with compilers much. Furthermore, if the compiler can recognise that the assembly routine is equivalent to the C implementation, wouldn't it also be able to generate the same routine?

>Is that something actual compilers can do right now?

it is not (outside of research)

>if the compiler can recognise that the assembly routine is equivalent to the C implementation, wouldn't it also be able to generate the same routine?

If you're willing to provide the equivalence proof yourself, it is much easier to verify such a proof than to produce one. The more work you're willing to put in when writing it, the simpler the proof verifier becomes. You could probably write a basic school arithmetic proof verifier within an hour or so (but it would not be pleasant to use).

I've thought about this idea a lot myself and I think it should be feasible, (maybe not with assembly right away). You could write an easily readable function in C for code review/verification purposes and then specify a list of transformations. Each transformation must preserve the semantics of the original function. For example "unroll this loop by a factor of 4", "Fuse these 4 additions in a single vector instruction". It would be a pain to write such a transformation list (AI assistance maybe?) but once written you can rely on the compiler to make sure there are no mistakes.

I guess you could run roughly the same set of unit tests on both implementations even if you can't formally prove equivalence. The unit tests would likely need to be adapted a little for each implementation. Of course, you then need to prove that the two sets of unit tests are equivalent :)