News for hackers. Stuff that matters.

A comment on The SeL4 Foundation: What and Why. Parent comment

Re:The SeL4 Foundation: What and Why by vbezhenar on Tuesday April 07, 2020 @09:21AM (#22802937)
How will it prove that this new optimization does not introduce bugs? It's not like GCC is verified compiler.
[ Parent | on HN ]
Re:The SeL4 Foundation: What and Why by saithound on Tuesday April 07, 2020 @09:40AM (#22803093)
Great question. They don't have to trust the compiler: after compilation, they use an SMT-based proof process to establish that the resulting binary matches the semantics of the C source directly. See https://ts.data61.csiro.au/publications/nicta_full_text/6449....
[ Parent | on HN ]
Re:The SeL4 Foundation: What and Why by zingermc on Tuesday April 07, 2020 @11:16AM (#22803979)
Ah, it appears that is only done for ARM, but not x86. It would be great if x86 were more amenable to FM, or if we had faster formally-specified processors. Can't wait for a RISC-V workstation!
[ Parent | on HN ]