Yup, that's another way to do it so long as you're interested in paying the explicitness tax to introduce substructural types. My point about Hoare logic is not

Yup, that's another way to do it so long as you're interested in paying the explicitness tax to introduce substructural types. My point about Hoare logic is not to promote it but instead to note that it's not categorically different from equational reasoning except in that it operates over more complex languages. And then that exactly is your tradeoff.