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.
> 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.
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.... :)
Yeah, I've be _really_ impressed with Lean's support. Wish other provers like Coq and Agda were at the same level (I know how challenging it is to do though).
Proving systems are one of main areas of research in blockchain space; on different levels - at type level for contracts/vm, at consensus level regarding properties like liveness etc and at multiple cryptography levels ie. in area of zero knowledge computations.
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.