How Many Decimals of Pi Do We Really Need?

Of course, the real reason they work with pi to exactly 15 decimal places is that they're doing numerics, and therefore use a full double precision constant for pi, i.e., the number of decimal places that can be stored in a 64 bit float