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.

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:

• start with something fun and surprising, perhaps Paulo Oliva's tutorial on Programs from classical proofs via Gödel's dialectica interpretation

• an accessible paper on realizability interpretation which uses logical methods in computable analysis might be Ulrich Berger's Realisability for Induction and Coinduction with Applications to Constructive Analysis

• if you want to use computers to actually show correctness of programs, you could learn Coq and then proceed to Ynot (Hoare logic on steorids) or go straight to Adam Chipala's Certified Programming with Dependent Types.

• cool people use Agda instead of Coq.

• if you are first-order logic sort of person, you might find Minlog more palatable than Coq and Agda, as it does not throw type theory in your face.

See you in two years.