I would argue "reasoning about programs" formally means "can prove P Q R ..." (with appropriate choices for P Q R) and doesn't implicitly carry an assumption of consistency. But, fair enough.
You make a good point, and on the other hand you're right that "reasoning about programs" is not a term of art, so who knows what it means. Given how Lean is used in the article, I took it as basically being some kind of Turing-complete language (lambda-calculus or some variant or what-not).
