sergevar

Yep, thanks!

A good process deletes decisions (the Glasgow northbound rule) by focusing you on exactly the steps you need to take. A bad one might remove a few but spawn fifty more (suddenly you're debating story points/t-shirt sizes, velocity arguments, Definition of Done, but hey, at least you know it's all scheduled to start at 09:30)

Interestingly, there was a Show HN last year formalizing PM in Lean (https://news.ycombinator.com/item?id=43797256), and the Principia Rewrite project (https://www.principiarewrite.com) verified all 189 propositional logic theorems (sections 1-5) in Coq against the original proof sketches