Formal Reasoning About Programs (2017) [pdf]

The current wave of ML techniques are approaching a plateau. The current approach is use deep learning, then iterate by adding fancier models / more data / more compute. That loop has diminishing returns on time/$ spent, so it's now time for the next big value jump, similar to when DL models started to relatively easily outperform Bayesian models on certain problems.

Interestingly, both the problem domain of what to solve, and how fancy solutions work, increasingly looks a lot like programs. Relational learning, automation, ...

A growing subfield in the proof world is Program Synthesis, which looks at all sorts of techniques to do just that. Two lessons from there has been proof solvers can get you quite far, and increasingly, that you can combine traditional logic solvers with ML techniques to great benefit. If I was OpenAI, I'd take Microsoft's $1B and spend less on running bigger models and people doing incremental tweaks to them and a LOT on people working here.

(I do think proofs-for-programs also has bigger adoption hopes in areas like security, but that's a much more nuanced and domain-specific story. Meanwhile, we do see continued niche success for more niche NASA and DoD style work, so the small money train will continue driving the community's focus on stuff like OS verification.)

I have an MSc where I focused in formal methods and I worked pretty extensively with them both in academia and industry before moving to machine learning, getting another MSc and a PhD.

There are many formal methods industrial users, especially those dealing with hardware and safety critical systems. For them, the cost / benefit ratio of using formal methods makes a lot of sense.

My hope is that lightweight approaches become more polished and it becomes feasible to use them in more mainstream applications. There is a whole range of methods going from type and effect systems, model checking, data and control flow analysis all the way to abstract interpretation and theorem proving. For example, refinement types as implemented in Liquid Haskell are a nice promising area.

I also think there are potentially very interesting combinations of deep learning and probabilistic inference plus formal methods that might push both AI and software engineering further. For example, an intelligent agent that is trying to infer (synthesize or induce) a program that models some function [1] might be able to carry a much better search by using abstract interpretation.

[1] https://www.sas.upenn.edu/~astocker/lab/teaching-files/PSYC7...

The tool could do formal proofs, although when I left it wasn't used in the way theorem-prover people seem to imagine them being used: starting by a full model of what the workpiece should do. Instead, it was used to prove assertions were always/never true. But in HW we have a lot of assertions :-)

For software there are a couple of issues: one is that the state is a lot bigger (in theory of course HW state is a superset of SW state, but in practice the content of most RAM can be regarded as just content and you don't need to prove anything about it other than that it is copied okay).

The other is that with the skimpy amount of testing most teams do, there isn't a huge pressure to find a way to reduce testing costs like there is in HW (where 2 engineers writing tests to one writing verilog isn't unusual).

Well, we’re hiring those skills into one of the world’s larger banks. As are peers with similar industry challenges.