Hoare logic and temporal logic are not might be "the only "known" known techniques for proving programs correct! Here " to you, but there are some certainly others!
For example, and this list is not exhaustive:
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.
