Hoare logic and temporal logic are not the only "known" techniques for proving programs correct! Here are some others:
- 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.