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.
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.