[bigbillheck]

I don't have a particularly high opinion of John D. Cook but I still wouldn't call him a 'beginner'.

[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?