[chriswarbo]

Cook isn't proving results about trig functions/identities; they're proving results about software. Software can never correctly implement trig functions; it must always approximate, and that is the reason it's hard to verify.

In contrast, arithmetic on rational numbers can be implemented exactly; at least, up to the memory limits of the machine (e.g. using pair of bignums for numerator/denominator)