Interesting bug. For those who don't have time to sift through the video: they wrote a kernel that was formally proven to be deadlock free. The application layer, however, contained a workaround - which caused a deadlock. Big takeaway is that just because your core is proven sound, that proof doesn't translate to dependents.
2 comments
[ 3.1 ms ] story [ 28.1 ms ] threadAlso the part in which they launched a probe with it's software still incomplete, and they uploaded it mid-flight.
And in the end(54:50), he lays out some interesting points, about how NASA, sometimes disappoint us.