Hacker News Reader

Comment by arxanas | Hacker News Reader

Rice's theorem states that there is no general procedure to determine if an arbitrary Turing machine has some property. We are restricting ourselves to programs which typecheck under a certain type system, so there will certainly be a class of properties it can guarantee while still being Turing-complete (such as the bounding of memory, CPU, etc.). That is to say that it's not "theoretically possible in the general case," but we are willing to work with more specific cases, so it's not relevant to invoke Rice's theorem in this situation.

View on HN

> 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!

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.

I think you're being overly reductive:

> Using Rogers' characterization of acceptable programming systems, Rice's theorem may essentially be generalized from Turing machines to most computer programming languages: there exists no automatic method that decides with generality non-trivial questions on the behavior of computer programs.

https://en.wikipedia.org/wiki/Rice%27s_theorem

I don't understand why you say that my comment is reductive. It's adding nuance to the topic at hand, rather than removing it. The original comment talks about a situation where we constrain ourselves to "rigid types"; the child comment remarks on Rice's theorem having consequences for the analysis of general Turing machines; and I remind the commenter that we have already restricted ourselves to Turing machines satisfying some type system.

Another way to express the same point of view is to say that I am arguing that the Curry-Howard isomorphism is more relevant to the situation at hand than Rice's theorem. (This might be the "promise" that the original commenter was referring to.)

Reply on news.ycombinator.com