Remix.run Logo
rwmj 3 hours ago

However you can do what Airbus do and formally prove your C code and use a formally proven toolchain like compcert to compile it. Or you can take a performance hit and add bounds checking to the C code[1]. Aircraft systems are probably the best chance that CHERI has, and that's pretty niche, small runs and very expensive, and still better solved in software.

[1] I literally wrote the paper on this back in 1996: https://www.doc.ic.ac.uk/~phjk/BoundsChecking.html

pjmlp an hour ago | parent [-]

Most people on HN would run screaming away if they had to follow high integrity computing processes on their daily C programming.

If they think programming with Modula-2 and Object Pascal is programming with a straightjacket, good luck with MISRA, Frama-C, DOD and ISO certifications for reliable C code.

ykonstant 32 minutes ago | parent [-]

For the record, I found programming in MISRA C guidelines really fun; but then again, I did it out of personal interest. If I had to do it professionally, I guess the pressure would be less pleasant.