3 ms·

> I get that being able to check for non-termination would be useful—but is there more? It's not just that "there is more", it's that there is everything. Th

by drostie 10y ago

> I get that being able to check for non-termination would be useful—but is there more? It's not just that "there is more", it's that there is everything. The halting problem which we're talking about here is actually easily generalizable into a set of generic theorems about static analysis of programs in general. The usual first step is to prove the first incompleteness theorem (no axiom system proves all of the interesting facts about the integers), then modify that into a proof of the second incompleteness theorem (that every logic which proves its own consistency must be inconsistent). But it goes way further than that to Rice's theorem: every nontrivial semantic property of a computer program is undecidable. Put another way, the only way for the compiler to know that something is true is for there to be a really simple up-front convention which makes it true. Suppose you want to make sure, statically, that you never dereference a null pointer. This says that the only way a compiler could ever be strong enough to prove this is if it's syntactically impossible to create a null pointer in the language in the first place, so that it's a "trivial property" of all programs that they never dereference null pointers. Suppose you want to prove that a certain block of code is the fastest possible code which does a certain thing. The only ways to do this require the language to "normalize" all of its expressions so that there is only one block of code for everything you want to do. If there's more than one way to do it, then the analysis "is this the fastest code?" is nontrivial and you can't prove it! (You can always get heuristics of course to try to cover the most common cases, but your heuristics will never cover everything you want.) Suppose Microsoft wants to fix Word and Excel's macro systems to a new form that cannot contain viruses: the only way to do that is if the macro system is either (a) Turing-incomplete, so that you can analyze its programs, or else (b) unable to do the virusy things that you're worried about in the first place. Otherwise there will always be a macro-virus which passes the virus-checker.

skybrian 10y ago
In theory, sure. In practice, a program that takes a century to run is indistinguishable from a non-terminating program. If you prove a macro is safe by trying every possible combination then it could very well take that long. And we usually don't wait that long. A function that executes when loading a web page times out in the order of seconds. Once you have deadlines, all bets are off - the function is not deterministic for any large enough input. Equational reasoning does not preserve performance - it could cause a program that previously ran fast enough to time out. So, knowing that function terminates seems only theoretically useful. It doesn't tell us whether a program change is really safe. It would be more useful to put some kind of bound on the resources a function can consume. In Etherium's language, there is a concept of "gas" which is an abstract limit on how much work a function can do. (The advantage over a timeout is that it's not machine-specific.) I sometimes wonder if anyone has applied this concept to functional programming? Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas?
- chriswarbo 10y ago
  > Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas? Have a look at areas like "cost semantics", e.g. http://lambda-the-ultimate.org/node/5021 http://lambda-the-ultimate.org/node/5021 This takes a language's semantics, i.e. how to evaluate each sort of expression, and extends it to include extra information which can represent time taken, memory usage, cache usage, etc. A simplistic way to track big-O complexity in types is given at http://twanvl.nl/blog/agda/sorting http://twanvl.nl/blog/agda/sorting Note that "gas" systems don't need to produce their result within the given gas limit; it's acceptable for the gas to run out and no value to be produced. This is trivial to prove correct, as it only requires that the language/DSL correctly keeps track of the gas, which can be done "once and for all" since it doesn't have anything to do with whatever algorithm you're writing to use the gas. The machinery for doing that is old hat to functional programming: tracking gas usage is basically a Writer; stopping when gas runs out is basically a Maybe. Statically ensuring that a function is within a gas limit is like statically ensuring that a "Maybe t" value contains a "t" value (as opposed to "Nothing").
  - pron 10y ago
    > This takes a language's semantics, i.e. how to evaluate each sort of expression, and extends it to include extra information which can represent time taken, memory usage, cache usage, etc. This simply says that functional languages could be assigned cost semantics, just like imperative languages have, and so may be used for algorithm analysis. It has nothing to do with verification. > tracking gas Yep, but that's a trivial property that could be done by any runtime. It doesn't help prove any other correctness property.
pron 10y ago
> It's not just that "there is more", it's that there is everything. The halting problem .... No, no, no. The original halting theorem is avoided in total languages, but the much more important version which forms the core of the time-hierarchy theorem, sometimes known as "bounded halting", holds unchanged. It is a generalization of halting which basically says that you cannot know anything about a program (including halting) any faster than running it (more precisely, you cannot know whether a program P halts in input x within n steps in fewer than n steps; all the other corollaries like Rice follow in the same way). This means that the cost of verification is the same for total and non-total programs, with the theoretically interesting but pragmatically irrelevant promise that the cost is some unbounded finite number in the total case. If you want to convince yourself that totality cannot make proving program properties easier with an intuitive argument, consider this: take any program ever written, and to every loop and every recursive call add a counter initialized to 2^100 that is decremented with every iteration/recursion and stops the program when it reaches zero (which will not happen until the end of the universe). Your program is now provably total, yet its semantics have not changed a bit. I.e., you can already assume without loss of generality that every program is a total program and that every language is a total language. Is verification easier now that you know this? The only case where you cannot make this assumption is when your language is used as a theorem prover to prove general mathematical theorems (that aren't executed and may actually "reach" infinity), and this is where totality matters. See my post for a more in-depth discussion: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
- drostie 10y ago
  This looks like a long blog post but I will be happy to read it. ^_^

by drostie 10y ago

skybrian 10y ago

In theory, sure. In practice, a program that takes a century to run is indistinguishable from a non-terminating program. If you prove a macro is safe by trying every possible combination then it could very well take that long. And we usually don't wait that long. A function that executes when loading a web page times out in the order of seconds. Once you have deadlines, all bets are off - the function is not deterministic for any large enough input. Equational reasoning does not preserve performance - it could cause a program that previously ran fast enough to time out. So, knowing that function terminates seems only theoretically useful. It doesn't tell us whether a program change is really safe. It would be more useful to put some kind of bound on the resources a function can consume. In Etherium's language, there is a concept of "gas" which is an abstract limit on how much work a function can do. (The advantage over a timeout is that it's not machine-specific.) I sometimes wonder if anyone has applied this concept to functional programming? Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas?

chriswarbo 10y ago
> Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas? Have a look at areas like "cost semantics", e.g. http://lambda-the-ultimate.org/node/5021 http://lambda-the-ultimate.org/node/5021 This takes a language's semantics, i.e. how to evaluate each sort of expression, and extends it to include extra information which can represent time taken, memory usage, cache usage, etc. A simplistic way to track big-O complexity in types is given at http://twanvl.nl/blog/agda/sorting http://twanvl.nl/blog/agda/sorting Note that "gas" systems don't need to produce their result within the given gas limit; it's acceptable for the gas to run out and no value to be produced. This is trivial to prove correct, as it only requires that the language/DSL correctly keeps track of the gas, which can be done "once and for all" since it doesn't have anything to do with whatever algorithm you're writing to use the gas. The machinery for doing that is old hat to functional programming: tracking gas usage is basically a Writer; stopping when gas runs out is basically a Maybe. Statically ensuring that a function is within a gas limit is like statically ensuring that a "Maybe t" value contains a "t" value (as opposed to "Nothing").
- pron 10y ago
  > This takes a language's semantics, i.e. how to evaluate each sort of expression, and extends it to include extra information which can represent time taken, memory usage, cache usage, etc. This simply says that functional languages could be assigned cost semantics, just like imperative languages have, and so may be used for algorithm analysis. It has nothing to do with verification. > tracking gas Yep, but that's a trivial property that could be done by any runtime. It doesn't help prove any other correctness property.

pron 10y ago

> It's not just that "there is more", it's that there is everything. The halting problem .... No, no, no. The original halting theorem is avoided in total languages, but the much more important version which forms the core of the time-hierarchy theorem, sometimes known as "bounded halting", holds unchanged. It is a generalization of halting which basically says that you cannot know anything about a program (including halting) any faster than running it (more precisely, you cannot know whether a program P halts in input x within n steps in fewer than n steps; all the other corollaries like Rice follow in the same way). This means that the cost of verification is the same for total and non-total programs, with the theoretically interesting but pragmatically irrelevant promise that the cost is some unbounded finite number in the total case. If you want to convince yourself that totality cannot make proving program properties easier with an intuitive argument, consider this: take any program ever written, and to every loop and every recursive call add a counter initialized to 2^100 that is decremented with every iteration/recursion and stops the program when it reaches zero (which will not happen until the end of the universe). Your program is now provably total, yet its semantics have not changed a bit. I.e., you can already assume without loss of generality that every program is a total program and that every language is a total language. Is verification easier now that you know this? The only case where you cannot make this assumption is when your language is used as a theorem prover to prove general mathematical theorems (that aren't executed and may actually "reach" infinity), and this is where totality matters. See my post for a more in-depth discussion: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...

drostie 10y ago
This looks like a long blog post but I will be happy to read it. ^_^