How much Coq do I need to know to learn SF Hoare Logic?

How much of the first chapter of SF do I need to know to tackle Hoare logic?
in volume 2
or which chapters of volume 1 are a must for Hoare Logic?

I’d recommend following the Chapter Dependencies. If you’re in a hurry, the informal explanations are well-written for you to understand Hoare Logic without knowing Coq. The syntax for inference rule was introduced in IndProp chapter. Maybe @bcpierce could provide better suggestions.


I really wanted to learn it WITH coq though, hence my question. Though, thanks for the response! :slight_smile: