Yes, absolutely. There's been a lot of work along these lines in other interactive theorem provers like Isabelle/HOL and Rocq. The general term to search is "Hoare logic," and I'm also a fan of the Concrete Semantics textbook. Lean is a very flexible language, but the main downside with Lean is that libraries for reasoning about program logic are comparatively less developed than Mathlib is for math.