The cutting edge of formally verified hard-realtime safety-critical software is academic and open source. I would only want to ride in a flying car if its contr

The cutting edge of formally verified hard-realtime safety-critical software is academic and open source. I would only want to ride in a flying car if its control code was written by public cooperation and was publicly auditable. The last thing I want is for people to ride around in missiles powered by Windows Embedded or Java SE Embedded, contracted out from Chevy to some software farm in India, with no public oversight except for the fact that Chevy's lawyers can convince the NHTSA that it satisfies whatever harebrained safety checklist the government came up with. Avionics is a special case in terms of cost, level of automation, homogeneity of products, and level of pilot expertise, which makes the use of some one-off Ada software Boeing wrote 30 years ago much more reasonable.