Wow. Finally a prover with serious IDE support.
I always believe this field would be very useful and evolving steadily in the industry. It just doesn't attract eyeballs like machine learning and blockchains.
I always believe this field would be very useful and evolving steadily in the industry. It just doesn't attract eyeballs like machine learning and blockchains.
... yet. The next AI Winter is right around the corner. While there has been seriously amazing work coming out of ML, in industry there is an insane amount of resources being put into completely BS ML systems. Outside of FAANG there are many "fancy" ML projects in industry that are just continually accruing massive technical debt, and for no good reason. The number of deep neural networks being used for problems that can be solved with radically much more simple (and easier to debug and maintain) techniques is astounding. Right now there is a boom in complex and fragile a systems made by teams of PhD in non-engineering fields that don't know anything about system or software design.
In a few years these complex systems will need to be maintained and fixed and it will quickly become apparent that the vast majority of these projects are a huge business liability with minimal financial or engineering benefit. Expect a huge back lash against predictions coming from complex, non-interpretable linear algebra heaps.
The pendulum will swing back, and likely pretty hard (as always probably too hard). I'm not sure theorem provers will be the winner, but the general class of understandable, predicable, and explainable things will become more popular. It is quite possible that "my tool proves things are stable and work" will be a big sell in the next wave of tech.
It would be fun in a TheDailyWTF way :)
Stories of AI Failure and How to Avoid Similar AI Fails in 2019 https://www.lexalytics.com/lexablog/stories-ai-failure-avoid...
How IBM Watson Overpromised and Underdelivered on AI Health Care https://spectrum.ieee.org/biomedical/diagnostics/how-ibm-wat...
Automakers Are Rethinking the Timetable for Fully Autonomous Cars https://www.designnews.com/electronics-test/automakers-are-r...
As an aside, my worry with AI/ML is that we’re creating these giant, un-debuggable systems that can’t be fixed when specific problems arise. Every time I see complaints about YouTube/Facebook/<some other company> giving nonsense recommendations to people I think “How would they even fix that? Do they even know how their recommendation systems work?”.
One of the great things about software is that when something is broken, you can go right in there and fix it. With ML, I can imagine getting to a point where our only option is to take the black-box we’ve created to therapy and hope for the best.... :)
https://leanprover.github.io/about/ https://github.com/leanprover/vscode-lean