[eesmith]

I apologize. I misread the context of the thread. I mistakenly though you were commenting on Wildberger's reasoning for promoting rational trigonometry, rather than on Cook's decision to use that approach.

If "formal verification" involves using a software-based proof assistant or automatic theorem prover then perhaps that easier to encode for those tools via rational trigonometry?

Why not ask him directly?