News for hackers. Stuff that matters.
Re:The Hundred-Year Language (2003) by millstone on Monday March 20, 2017 @03:52AM (#13912457)
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.

Re:The Hundred-Year Language (2003) by throwaway729 on Monday March 20, 2017 @08:42AM (#13913590)
> 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+...