Writing software for space probes

johndcook.com

30 pointsORioN632 comments

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.

Don'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.

Reply on news.ycombinator.com