News for hackers. Stuff that matters.

A comment on Sel4: We’re going open source. Parent comment

Re:Sel4: We’re going open source by Avshalom on Tuesday June 24, 2014 @02:52PM (#7939691)
On that note: what even is a correct translation of C when it has so many undefined behaviors in it's spec.
[ Parent | on HN ]
Re:Sel4: We’re going open source by cc_ on Tuesday June 24, 2014 @10:16PM (#7941904)
They use a formally-specified subset of C described in Harvey Tuch's PhD thesis: http://www.ssrg.nicta.com.au/publications/papers/Tuch:phd.pd...
[ Parent | on HN ]
Re:Sel4: We’re going open source by wmf on Tuesday June 24, 2014 @03:06PM (#7939809)
What if the code doesn't rely on undefined behavior?
[ Parent | on HN ]
Re:Sel4: We’re going open source by regehr on Tuesday June 24, 2014 @04:02PM (#7940197)
Absence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.
[ Parent | on HN ]