Formal reasoning about functional programs in terms of their (denotational) semantics is normal in a functional programming class (e.g. it's about a quarter of our mandatory-for-undergrads FP course).

Formal reasoning about imperative programs in terms of their (e.g. axiomatic) semantics is only in a grad-level course, and the programs you can reason about are really, really limited compared to the functional ones. (The last time I TA'd the FP class, one of the homeworks involved proving a simple compiler correct. When I took the grad course, I think the most complicated program we proved correct was selection sort.)

I think "reasoning about programs" is more computer-science than "writing programs," and choosing an imperative language signals that you're not emphasizing the former.

It's one way of modelling the broad notion an algorithm, but it isn't the only one, and it's odd to treat it as the one true expression of computer science when essentially all modern computing follows a different model.