I'm super bullish, but for a bit further out and for a different reason than the vast bulk of PL folks: a major value jump in AI.
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.)