5 ms·

> But there is, at least a theoretical, promise that when you are rigid enough in your types, you are able to predict & prove memory, cpu, network use etc. No,

by kaba0 3y ago

> But there is, at least a theoretical, promise that when you are rigid enough in your types, you are able to predict & prove memory, cpu, network use etc. No, that’s not even theoretically possible in the general case, see Rice’s theorem (at least if you stick to Turing complete programs), which states that every non-trivial (semantic) property of a program is undecidable.

arxanas 3y ago
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.
- kaba0 3y ago
  > 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!
  - markusde 3y ago
    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.
  - arxanas 3y ago
    For the case of resource usage, you can see work like https://link.springer.com/chapter/10.1007/978-3-030-81685-8_37 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.
  - jerf 3y ago
    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.
  - jfoutz 3y ago
    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.
- Ygg2 3y ago
  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 https://en.wikipedia.org/wiki/Rice%27s_theorem
  - arxanas 3y ago
    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.)
markusde 3y ago
This is a good but also misunderstood point. It is true that you can't automatically do this in general. However, expressive enough type systems can contain human-written, machine-checked proofs of (models of) these properties. I think the jury's still out on whether or not humans or machines are better at coming up with proofs, but computers are decisively a lot better at checking them than we are. The way I see it formal methods not a holy grail where we don't have to think about the code we're writing anymore, but it is a very strong next step from "I wrote this code and here's why I think it's right" to "I wrote this code and here's a machine-checked proof that it's right". Effective automation can make that step easier to take in a lot of real-world cases.
- kaba0 3y ago
  It’s not about automatically doing it — it’s about for many cases there can’t exist a proof. And it is not even some theoretically interesting but never happening case, but quite trivial programs will quickly come to this state. Sure you can restrict some things, like boundless loops, but the “beauty” of complexity and the limit of our very mathematics won’t disappear, unless you go to too trivial systems which are useless. See my other comment for an example. I remember there being an analogy between Gödel’s incompleteness theorem as well, which is also only true to “expressive enough” systems (where you can basically do integer math) — but I may be talking completely out of my arse at this point.
  - markusde 3y ago
    I get your point, and I agree with it too. My comment is (trying to) say that in those cases we don't know that humans are any better! Your other comment has some problems, but a better example is fn collatz(mut n: bigint, mut v: Vec<...>) { loop { n = { if n%2==0 then n/2 else 3\*n+1 }; v.push(...); } } As far as we know, we can't bound the memory usage of this program: and if any FM can do it as well then there's a million bucks on the table. But so far no human can do it either! And if your program relies on this program using bounded memory, from an engineering perspective you're kind of SOL no matter what. On the other hand, if you're writing programs which humans are pretty sure they know why the properties they want hold (as we usually try to do, anyways), then translating this into a machine-checked proof can give you a lot more faith that the property actually holds and possibly even find flaws in your reasoning/implementation if there are any!
jerf 3y ago
"(at least if you stick to Turing complete programs)" Many people interesting in this sort of formal proof community are actually perfectly willing to eject that. There's been a lot of interesting research into it. I think you can also ring-fence chunks of a program as being non-Turing complete and prove things about those chunks even if the program as a whole is Turing complete. That said, so far everything I've seen them produce involves a level of programming difficulty comfortably above writing real-world code in Haskell. For example, you do not have to learn category theory in the slightest to learn Haskell, but you will be learning a lot of real mathematical theories, of which group theory is probably one of the easier ones, to use these systems. They're working on that issue. But it has a long ways to go and it is not clear to me that the gap between these systems and the "programmer on the street" is anything that can ever be solved. Or, to put it another way in more engineering terms, I do not question the advertised benefits when advocates like the original author pitch them. They're real and exist in real, concrete systems that you can use today. However, the costs are grotesquely undersold. I'm not sure even the advocates really understand how far out of the loop they are on the costs of their systems. So far the costs end up choking you out on systems that conventional programmers would consider tiny. My browser may not be mathematically proved to not have security vulnerabilities, and it's certainly not free of bugs, but in the meantime, conventional programming has produced it and it's out there in the world bringing benefits today, not in however many decades or even centuries we are away from having something like a browser-sized program come with proofs of security and resource usage.
ashton314 3y ago
Type systems push semantic properties into syntactic ones, thereby making them decidable. Note that there are halting programs which will fail to type check, but that’s the trade off.
- kaba0 3y ago
  > Type systems push semantic properties into syntactic ones Ordinary types are so-called trivial properties though, so Rice’s theorem doesn’t apply to them.
  - mrkeen 3y ago
    You can get a lot better than trivial. Transactions for instance.
  - consilient 3y ago
    This isn't right: `int -> Zero` is an "ordinary" type, but certainly does not correspond to a trivial property. The reason Rice's theorem doesn't apply to types is that they're not purely "semantic" in the relevant sense, since they're not fully determined by the language a TM accepts.
    - kaba0 3y ago
      What type system do you imagine having that type signature? Zero being a value is usually exempt from the type system (unless we have dependent types, but I would definitely not call those ordinary). Of course if it’s a special type with only a single elem with no relation to int, then it is again trivial.
      - ashton314 3y ago
        Typed Racket (not a dependently typed system mind you) has zero as a type. It’s a fantastically useful type to have.
      - consilient 3y ago
        Any language with function types and singletons. > Of course if it’s a special type with only a single elem with no relation to int, then it is again trivial. No, it isn't. "Trivial" in the context of Rice's theorem means either true of all Turing machines or false of all Turing machines.
JonChesterfield 3y ago
The general case is for arbitrary programs. That's not the important case. You want to prove things about _this_ program which you've written, not about all programs.

by kaba0 3y ago

arxanas 3y ago

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.

kaba0 3y ago
> 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!
- markusde 3y ago
  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.
- arxanas 3y ago
  For the case of resource usage, you can see work like https://link.springer.com/chapter/10.1007/978-3-030-81685-8_37 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.
- jerf 3y ago
  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.
- jfoutz 3y ago
  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.
Ygg2 3y ago
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 https://en.wikipedia.org/wiki/Rice%27s_theorem
- arxanas 3y ago
  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.)

markusde 3y ago

This is a good but also misunderstood point. It is true that you can't automatically do this in general. However, expressive enough type systems can contain human-written, machine-checked proofs of (models of) these properties. I think the jury's still out on whether or not humans or machines are better at coming up with proofs, but computers are decisively a lot better at checking them than we are. The way I see it formal methods not a holy grail where we don't have to think about the code we're writing anymore, but it is a very strong next step from "I wrote this code and here's why I think it's right" to "I wrote this code and here's a machine-checked proof that it's right". Effective automation can make that step easier to take in a lot of real-world cases.

kaba0 3y ago
It’s not about automatically doing it — it’s about for many cases there can’t exist a proof. And it is not even some theoretically interesting but never happening case, but quite trivial programs will quickly come to this state. Sure you can restrict some things, like boundless loops, but the “beauty” of complexity and the limit of our very mathematics won’t disappear, unless you go to too trivial systems which are useless. See my other comment for an example. I remember there being an analogy between Gödel’s incompleteness theorem as well, which is also only true to “expressive enough” systems (where you can basically do integer math) — but I may be talking completely out of my arse at this point.
- markusde 3y ago
  I get your point, and I agree with it too. My comment is (trying to) say that in those cases we don't know that humans are any better! Your other comment has some problems, but a better example is fn collatz(mut n: bigint, mut v: Vec<...>) { loop { n = { if n%2==0 then n/2 else 3\*n+1 }; v.push(...); } } As far as we know, we can't bound the memory usage of this program: and if any FM can do it as well then there's a million bucks on the table. But so far no human can do it either! And if your program relies on this program using bounded memory, from an engineering perspective you're kind of SOL no matter what. On the other hand, if you're writing programs which humans are pretty sure they know why the properties they want hold (as we usually try to do, anyways), then translating this into a machine-checked proof can give you a lot more faith that the property actually holds and possibly even find flaws in your reasoning/implementation if there are any!

jerf 3y ago

"(at least if you stick to Turing complete programs)" Many people interesting in this sort of formal proof community are actually perfectly willing to eject that. There's been a lot of interesting research into it. I think you can also ring-fence chunks of a program as being non-Turing complete and prove things about those chunks even if the program as a whole is Turing complete. That said, so far everything I've seen them produce involves a level of programming difficulty comfortably above writing real-world code in Haskell. For example, you do not have to learn category theory in the slightest to learn Haskell, but you will be learning a lot of real mathematical theories, of which group theory is probably one of the easier ones, to use these systems. They're working on that issue. But it has a long ways to go and it is not clear to me that the gap between these systems and the "programmer on the street" is anything that can ever be solved. Or, to put it another way in more engineering terms, I do not question the advertised benefits when advocates like the original author pitch them. They're real and exist in real, concrete systems that you can use today. However, the costs are grotesquely undersold. I'm not sure even the advocates really understand how far out of the loop they are on the costs of their systems. So far the costs end up choking you out on systems that conventional programmers would consider tiny. My browser may not be mathematically proved to not have security vulnerabilities, and it's certainly not free of bugs, but in the meantime, conventional programming has produced it and it's out there in the world bringing benefits today, not in however many decades or even centuries we are away from having something like a browser-sized program come with proofs of security and resource usage.

ashton314 3y ago

Type systems push semantic properties into syntactic ones, thereby making them decidable. Note that there are halting programs which will fail to type check, but that’s the trade off.

kaba0 3y ago
> Type systems push semantic properties into syntactic ones Ordinary types are so-called trivial properties though, so Rice’s theorem doesn’t apply to them.
- mrkeen 3y ago
  You can get a lot better than trivial. Transactions for instance.
- consilient 3y ago
  This isn't right: `int -> Zero` is an "ordinary" type, but certainly does not correspond to a trivial property. The reason Rice's theorem doesn't apply to types is that they're not purely "semantic" in the relevant sense, since they're not fully determined by the language a TM accepts.
  - kaba0 3y ago
    What type system do you imagine having that type signature? Zero being a value is usually exempt from the type system (unless we have dependent types, but I would definitely not call those ordinary). Of course if it’s a special type with only a single elem with no relation to int, then it is again trivial.
    - ashton314 3y ago
      Typed Racket (not a dependently typed system mind you) has zero as a type. It’s a fantastically useful type to have.
    - consilient 3y ago
      Any language with function types and singletons. > Of course if it’s a special type with only a single elem with no relation to int, then it is again trivial. No, it isn't. "Trivial" in the context of Rice's theorem means either true of all Turing machines or false of all Turing machines.

JonChesterfield 3y ago

The general case is for arbitrary programs. That's not the important case. You want to prove things about _this_ program which you've written, not about all programs.