Compiling down to asm, lot of information is lost regarding memory layout etc, so it's not the best source for generating code.
edit: you also have mrustc as a Rust to C compiler outright.
Edit: Sorry I misremembered, they seem to compile C/C++ code to WASM then back to C: https://hacks.mozilla.org/2021/12/webassembly-and-back-again...
Although technically the plugins could be written in Rust.
I'd be curious to see the output! It'd be funny decompiling the rust compiler to C, then running it on another platform that way. (Though it would still be, for example, an x86 rust compiler running on arm).
That's an example of "lost in translation" as we don't know if the original source required ordering or not. x86 cannot express the weakest memory model supported by C.
I don't think this would work, unless the c file just contains inline assembly.
Not that the C will be much more readable than the dissassembly, but there's a chance less information will be lost.
How about formally verified SPARK code?
Are you aware of the scope of SPARK's assurances? You can't accidentally dereference a NULL pointer in verified SPARK code, for instance.
For instance, if you write your own proof and then prove the program meets it, there could still be a logic error in your proof.
Also, "in verified code" is a big loophole enough to leave security issues in - for instance a web browser (probably the thing you'd most like to prove security-issue-free) can still overwrite its own memory through things like OS image and font code, JavaScript JITs generating code to an insecure ABI you don't have a model for, syscalls to kernel code that can write back into your memory, etc.
Believing "formal" makes things magically correct does seem to be a common problem; it also comes up when people say something has a "formal audit" or needs to get one from someone. How do they "formally" audit it? Are they wearing suits?
Sure. Even mathematics research journals sometimes publish erroneous proofs. Practical formal methods generally rely on automated provers.
You're right though that software development using formal methods can still have a non-zero number of defects. AdaCore use the term ultra-low-defect software rather than bug-free software. For an interesting case-study see [0].
Unfortunately, even automated provers can have bugs. To my knowledge, all provers suitable for practical use are not themselves formally verified. I don't think this is often an issue in practice, though. It remains that formal methods have an excellent real-world track record. The 'problems' with formal methods aren't effectiveness, but effort/price, and perhaps scalability.
> a web browser (probably the thing you'd most like to prove security-issue-free) can still overwrite its own memory through things like OS image and font code, JavaScript JITs generating code to an insecure ABI you don't have a model for, syscalls to kernel code that can write back into your memory, but not effectiveness.
If you verify only certain parts of a software solution, then sure, you don't get formal assurances about its overall behaviour.
> How do they "formally" audit it? Are they wearing suits?
That's an entirely different use of the word, isn't it?
[0] https://www.adacore.com/tokeneer See page 59 of the (freely available) full report for Analysis section