Hacker News Reader

Comment by kaba0 | Hacker News Reader

> such as the bounding of memory, CPU

I don’t think any of those are possible (given that there is some construct in the language which will grow the memory) - how do you discern how many times will a given loop run?

For example, how much memory does this program use?

  int x = input().toInt()

  for 0..x {
    // something that allocates at least until the end of the loop
  }

And this is the very nicest case of a statically verifiably not infinite loop!

View on HN

For the case of resource usage, you can see work like https://link.springer.com/chapter/10.1007/978-3-030-81685-8_... "Synthesis with Asymptotic Resource Bounds" which implements bounded resource checking. Of course, there are programs it rejects that it can't prove, but this is the essence of type systems: if you are willing to appease the typechecker, then you can establish facts about runtime properties.

For your case, there may be a simpler dependently-typed solution: in such systems, you can already say things like "given an input natural number n determined at runtime, this functions returns a vector of size n", which bounds the result vector size. One approach could be to disallow explicit memory allocation and require passing a memory allocator as a parameter along with the associated "request" number bounding how many allocations you can do, in a similar dependently-typed way.

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.

It's not verifiable because you're trying to prove an incorrect spec! This program's memory usage is _not_ bounded above by a constant!

However, many modern formal methods _could_ prove that this function uses `f(x)` space, provided the loop body is simple enough.

I'm going to assert, you can calculate how much memory you'll need as soon as you see x. (maybe it's gnarly and complicated, but you can put an upper bound on it).

That number can be calculated at runtime. The program has access to the number, and you can make a choice about running that for loop or not.

The nifty bit is, the memory use information can be encoded in the type. the function has access to its type information. The compiler checks, and can make guarantees about your guard strategy - the actual values of available memory, and how much memory operating on x requires are only known at runtime. But the compiler can be check at compile time that the strategy is sound. maybe you have 5 bytes, maybe you have 5 gigs, who cares?

This can all be done without fancy languages, just write good code.

It's pretty nice to be able to throw more allocating function calls in the for loop, and have the compiler recognize that you're using (maybe) more memory, but your guard strategy is still good.

Reply on news.ycombinator.com