Although Lean 4 is a pure functional programming language, it is capable of expressing functions almost exactly like your example:
def isprime (n : Nat) : Bool := Id.run do
if n < 2 then
for i in [2:n-1] do
if n % i == 0 then
But you can argue that this is a cheat, since really lean is a functional language at heart, and this is true. What about "truly imperative" languages? Well, one issue with non-pure-functional languages is that functions are not pure, which means that you have to be careful about using them in specifications. What does the proof language even look like? Dependent type theory is one way to unify the concept of "writing programs" and "writing proofs"; in an imperative language these necessarily diverge.
It is, of course, possible to prove properties of imperative programs, but these tend to take the form of annotations around code, either using refinement types or design by contract style
ensures clauses around functions, loop invariants and other critical points in the code, with some automation to fill in the gaps. Why3 and Dafny are two strong examples of languages designed for reasoning about imperative code.