You build up abstractions in C by leveraging contracts and writing proofs of correctness based on those contracts. […] this course taught me how to reason about my programs

That seems like an essential part of what programming should be about? And imperative programming has it’s own considerations on how to go about it. I don’t see how it is a misnomer.