These days, there are compilers for embedded systems that can prove for certain code (for example) that it runs in constant time and constant space. As an examp

These days, there are compilers for embedded systems that can prove for certain code (for example) that it runs in constant time and constant space. As an example, galois.com has been doing this for Haskell, not just for embedded systems, but also for even more low level things like FPGAs.