Why Rocq is better than Lean for program verification

Especially now, with AI’s well-publicized success in mathematics, I get asked why I still use Rocq instead of giving in to the hype and switching to Lean. Most of this post started life as a provocati...