Proofs do not have to be of the form "This will never use more than 64 bytes of memory". You can prove that something will use x times 32 bytes of memory, or a

Proofs do not have to be of the form "This will never use more than 64 bytes of memory". You can prove that something will use x times 32 bytes of memory, or a polynomial value based on x, or whatever you have. Then you have to decide if that meets your needs or not. But this is also where they get tricky. You can have a proof that a particular sort function will never use more than twice the memory of what you pass in, and then you can combine that with a proof that some other bit of code will never have more than 10 elements, and that produces a proof that you only need 20 element's worth of memory for that upper function... but across an entire program, what sounds cute and useful in my little example here becomes its own monster of complexity. So far it is not yet clear to me that it constitutes an improvement on the underlying program.