[immibis]

Computers are imperative. With imperative programming you can get better performance than with pure functional. (Using pure functional to wrap an imperative core still counts as imperative)

Maybe you don't care about performance; IMO squeezing performance is one of the important applications for formal verification, as you can prove your fast insane algorithm is correct, whereas the slow obvious one is obviously correct.

If your main concern is clarity, some things are clearer when written imperatively and some when written functionally.