This is a project that aims to build systems that are provably immune to timing attacks. This is accomplished by using dependant types and the Curry-Howard isomorphism to have the program itself serve as the proof of its time constancy. At the moment the only function written is equality, and the proof is just that the same number of basic Boolean logical operations is performed, but the concept can be expanded to any function that can be expressed as a sequence of primitive boolean logical operations.
Everything is fairly broken right now as this is still really early pre-alpha
Accepted for presentation at THOTCON 2015!