Timing attacks are a huge problem for modern cryptosystems, having been successfully employed against AES, SSL, RSA, and many other cryptosystems we depend on to be secure. This talk presents a new method for writing code that is provably resistant to timing attacks using concepts from functional programming and type theory. This talk will go over some interesting pieces of math, crypto, and type theory and end up with a proof-of-concept provably constant-time program.