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.