5 ms·

What industries are using formal methods to not crash things? Honest question. What I see is the opposite - Uber and (to a lesser extent) Tesla cowboying their

What industries are using formal methods to not crash things? Honest question. What I see is the opposite - Uber and (to a lesser extent) Tesla cowboying their way towards autonomous vehicles. The idea of formally verifying a DNN image classifier seems absurd. And the old guard is even worse - recall Jeep's entertainment unit remote hack, or Toyota's 10,000 global variables? Those guys can't handle basic software engineering practices, let alone formally verified programs.

throwaway729 10y ago
> What industries are using formal methods to not crash things? Aerospace and chip design are the two major industries that make regular use of formal methods. > Uber and... Tesla... cowboying... And the old guard is even worse - recall Jeep... Yes, most of the auto industry has been slow to the table when it comes to taking software quality and capability seriously. Uber has a prototype, not a product, and Tesla has a young product. We'll see what engineering practices they adopt over the next 15 years. > The idea of formally verifying a DNN image classifier seems absurd https://www.google.com/search?q=verification+of+deep+neural+nets https://www.google.com/search?q=verification+of+deep+neural+...