I will first recall some computational interpretations of logic, with a focus on Gödel's Dialectica -- which plays a central role in concrete applications of proof theory to mainstream mathematics via the so-called "proof mining" program.

Then I will discuss some content from a recent joint work with Thomas Powell (University of Bath): we present Dialectica as a collection of rules inspired by Hoare logic ; in this way, Dialectica is viewed as a specification system for "procedural" programs that come with a forward and backward direction, and this viewpoint naturally captures the dynamics of extracted realisers from proofs. We also define a big-step semantics for (a fragment of) this system, that shows that Dialectica performs a generalised backpropagation.