This Dagstuhl Seminar seeks to extend and deepen the convergence across disciplinary boundaries by fostering exchange and collaboration among the relevant experts and practitioners, uniting expertise in proof theory with proof complexity, categorical semantics, constructive mathematics, proof mining, program extraction, and automated theorem proving. By bridging these domains, we seek to empower the next generation of researchers to frame and connect their work within this converging landscape, ultimately advancing the computational applications of proof systems in both theoretical and practical contexts.