I am looking to understand what Hoare logic is, and how it is used to prove program-correctness. I am interested in an applied text, which shows how to actually state formal specifications of programs, and prove that a program meets this specification using Hoare logic. But I’d also like to have a somewhat precise understanding of what Hoare logic actually is formally (i.e. how does it relate to other logics? Is it an extension of first-order logic? Is it constructive or classical? etc).
What is a good textbook/resource for me?