Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language (Logical Methods in Computer Science, 2024)