Hacker News Reader

my reticule aims at the creation of the formal C semantics being used to verify the output. If both you and I make an off-by-one, we can always agree on the (say, index) value, but we'll both be always wrong. And C semantics is something especially finicky, given how often we delve in "undefined behaviour" territory, or our nowadays hardware does something that "back then" was unthinkable.

View on HN

The formal C semantics are defined in Isabelle/HOL, checked, and then the compiler output is also checked. They use standard GCC compilers for all of this.

See https://riscv.org/blog/2021/05/sel4-on-risc-v-verified-to-bi...

Yes, making a mistake when writing down the C semantics is definitely possible. The point of the work announced here is to get rid of that risk, so that the proof only relies on the semantics of the RiscV instructions (and the C semantics become an intermediate thing which are proven rather than trusted). It's still possible that they made a mistake when writing down the RiscV semantics, but machine code is much simpler than C so the risk is smaller.

Reply on news.ycombinator.com