Skip to main content
2 of 2
link to Agda; added 56 characters in body
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

Hoare logic and temporal logic might be "the only known techniques for proving programs correct" to you, but there are certainly others!

For example, and this list is not exhaustive:

  • equational reasoning about fixpoints, this works in languages like Haskell
  • properties of programs can be proved via denotational semantics, which in itself is a vast area including domain theory and game semantics, to name just two.
  • for certain kinds of programs, for example for parametrically polymorphic ones, there are techniques that go under the name "relational parametricity"
  • you can use various logical interpretations to get correctness of programs:
    • a program extracted as a realizer via the realizability interpretation of logic automatically satisfies a certain specification
    • with tools such as Coq you can use type theory to write programs as proofs, or construct programs and prove them correct all at once
    • there are other ways of extracting programs from logical statements, one family of which are variants of Gödel's Dialectica interpretation that extract programs from classical logic.

Now, regarding your specific question. I think you should look at realizability, type theory, and extraction of programs from proofs. All of these are "logical" methods for developing correct programs, or proving them correct. Some randomly chosen starting points:

See you in two years.

Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239