Proof drives understanding of your code. That is why the resulting code is often small and clear. It pushes the field forward, but not in the direction you migh

Proof drives understanding of your code. That is why the resulting code is often small and clear. It pushes the field forward, but not in the direction you might think it does. You see, the shitloads of working code really works and solves problems. But you might not understand why. The work with proofs gets you closer to an understanding of the underlying why-question. And I don't think PL-research will ever catch up to the real-world experiments done in code. It took 40 years to embrace garbage collection for typical programs, so I don't have hope anything else will move soon.