¤ 1 if x == 1

¤ x * fac(x-1) otherwise"

This is at least more declarative than describing the function with a loop. With an imperative program you kind of have to describe as a series of steps, because the order matters so much.

Personally I prefer this kind of declarative programming over something like Prolog since I get a simple way of describing what/how the program is, while still feeling declarative. With Prolog I still have to learn how it works, and the way that it works is more removed from imperative and functional programming (while functional programming can be done (maybe with, but in principle) in most imperative languages as long as you restrict your use of certain features). Plus Prolog has un-declarative things like the cut operator. I don't really have much experience with declarative programming outside of these two.

Something more declarative might indeed just be to give invariants and let the program find an implementation for it.