3 ms·
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 la
by binarymax 15y ago
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.
- ORioN63 15y agoDon't forget the use of Lisp REPL, to actually solve it. I think it's pretty cool. Also 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.