It would be nice to be able to use the hardware timer peripherals to do this directly rather than relying on callbacks; I have already tried the callback approach, and even with external logic implementing a clock divider (a very old 74'163 binary counter chip) to get the frequency down to 50 kHz, I am finding that processing 50,000 callbacks per second is still too much for the pyboard.
My goal is to synchronize an OCVCXO (Oven-compensated, voltage controlled crystal oscillator) with the 1 Hz pulses from a GPS receiver. The OCVCXO is a high-precision oscillator that can be tuned with an external voltage source, and PPS output from the GPS comes very close to atomic clock precision, so it should be possible to tune the oscillator to generate exactly 12,800,000 oscillations per GPS pulse, at least as a long-term average. The only trick is to accurately count pulses and generate the analog compensation voltage.
If it is already possible to do this using the timer class, that would be great, but I haven't figured out how just yet. I would also be open to suggestions of a custom written C module or using inline assembler. Or, if anyone has reason to believe that the interrupt system on the STM32F405 has too much latency to do what I am attempting, then I would appreciate hearing that as well!

-Bryan