Insight

Stream: general

[Patrick Massot]

Do we know how much of https://www.youtube.com/watch?v=bGD_YF64Nwk has been formally certified?

[Scott Morrison]

Interesting question. I was wondering the same earlier today. Looks like it was certified enough. :-)

[Scott Morrison]

https://lars-lab.jpl.nasa.gov/

[Patrick Massot]

Indeed

[Patrick Massot]

https://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf is pretty scary reading. It makes me wonder why they still use C

[Patrick Massot]

(not that I know anything about this)

[Andrew Ashworth]

Embedded systems are still mainly programmed in C and assembly, since you need to interface directly with hardware

[Andrew Ashworth]

C++ is getting some traction though

[Kevin Buzzard]

How difficult can it be to formally verify C code? Doesn't C only have about 8 commands?

[Simon Cruanes]

C is pretty difficult to verify due to the tons of undefined behaviors, but people have done a lot of work on it. I'm more surprised that they never switched to Ada…

[Chris Hughes]

nat only has two.

[Kevin Buzzard]

nat only has two.

Yeah, but their behaviour is well-defined :-)

[Kenny Lau]

How difficult can it be to formally verify C code? Doesn't C only have about 8 commands?

... so... verify brainfuck?

[Keeley Hoek]

Most of those rules are more benign than I would have thought
Pretty sensible for any embedded system which wants to be careful I guess
Also, classic:

Rule 30 (type conversion)
Conversions shall not be performed between a pointer to a
function and any type other than an integral type.

[Keeley Hoek]

"Sorry team, I cast my function pointer to a double, then added five"