3 ms·

>I don't think it comes up much in practice because bugs due to non-terminating code don't actually happen much to begin with (compared to all bugs that cause h

>I don't think it comes up much in practice because bugs due to non-terminating code don't actually happen much to begin with (compared to all bugs that cause hangs or timeouts), and when they do they are often found via testing. We know that a function terminates for any inputs it was tested with. None of these are acceptable in Agda actually, since they would all be partial functions (i.e. functions that are not defined for some inputs.) The simplest, intuitive explanation is that since Agda has dependent types it needs to be able to evaluate functions during typechecking, and if you allow partial functions (e.g. infinite loops, halting functions, functions that timeout, or functions that are undefined for untested input) the typechecking would be undecidable. Instead Agda has a bunch of built-in tools to help the compiler figure out if a function is total (the opposite of a partial function, meaning it's defined for all possible inputs). Things like the termination checker can detect a subset of all terminating functions, and sized types let the programmer aid the compiler in figuring this out. There are also language pragmas to overide this totality check on a per function basis. I've implemented an algorithm, that I knew on paper terminated, and had it rejected by Agda, although I'm not experienced enough to know how easily these things are solved in general.

skybrian 8y ago
Yes, static analysis is very useful for understanding what the source code will do for inputs you didn't test. Testing is rarely exhaustive. However, testing will find performance issues where static analysis won't. To quibble with "none of these are acceptable in Agda": it seems unlikely that Agda or anything like it would detect hangs or timeouts due to code not meeting its deadline. Deadlines and performance constraints are not part of any type system I've ever heard of. Furthermore, performance is dependent on the compile toolchain, the runtime, and what else is running on the same machine, so it's not even well-defined for static analysis unless you make a bunch of deployment-specific assumptions. A language may guarantee that a function is total in a theoretical sense, but you might not be able to calculate its value for some inputs in practice. (Consider something like "a ↑↑↑ b".) So this guarantee is subtly different from what most users of computer systems would actually want. Of course, as a another commenter pointed out, this sort of practical bug-finding is not actually what the termination guarantee is for.
- joel_ms 8y ago
  > Yes, static analysis is very useful for understanding what the source code will do for inputs you didn't test. Testing is rarely exhaustive. However, testing will find performance issues where static analysis won't. Static analysis is a funny word to use about what Agda does.. Remember, Agda has dependent types, so what you're calling "static anaysis" involves evaluating/executing functions. In fact it needs to be able to evaluate/execute any functions beyond value-level in any imported modules just to be able to parse a sourcefile, due to the presence of mixfix-notation[0] and how it affects typechecking. > Testing is rarely exhaustive. However, testing will find performance issues where static analysis won't. How do you test a function that takes a natural number? Not an unsigned integer, but an actual countably infinite natual number? For every natural number n you test your function with, you can construct a new natural number n+1 which your function is untested for, (literally) ad infinitum. The answer, of course, is mathematical induction[1] and in the case of more general data structures we have the more general structural Induction[2]. But at this point you don't call it testing, you call it proving, and it's this that Agda is aspiring to. > To quibble with "none of these are acceptable in Agda": it seems unlikely that Agda or anything like it would detect hangs or timeouts due to code not meeting its deadline. Yes, your right that actually detecting hangs or timeouts would be difficult or impossible. But that's not what Agda does. Agda only allows functions that the compiler can figure out are total, which can never be all total functions (otherwise we would have a solution to the halting problem I think.) Basically, functions are either (provably total by the compiler) and hence acceptable. In the case of long/diverging computations Agda just has a timeout threshold, where it rejects a function if it takes too long to evaluate it during typechecking. I'm pretty sure that's what would happen if you tried "a ↑↑↑ b". > Of course, as a another commenter pointed out, this sort of practical bug-finding is not actually what the termination guarantee is for. Correct, it's not for bug-finding at all, but rather to keep the type theory/logic sound when using Agda as a proof assistant. Just to be clear: your criticism makes a lot of sense from a software engineering perspective, but considering the general performance characteristics of Agda, and the almost noneexisiting tooling around it, I think we're a couple of years away from "deployment specific assumtions" being something Agda needs to be too concerned about :) [0] You can define a function "if_then_else_" where the underscores represent arguments, so you would use it like this: "if TRUTH_VALUE then TRUE_CONSEQUENCE else FALSE_CONSEQENCE" [1] https://en.wikipedia.org/wiki/Mathematical_induction https://en.wikipedia.org/wiki/Mathematical_induction [2] https://en.wikipedia.org/wiki/Structural_induction https://en.wikipedia.org/wiki/Structural_induction

skybrian 8y ago

Yes, static analysis is very useful for understanding what the source code will do for inputs you didn't test. Testing is rarely exhaustive. However, testing will find performance issues where static analysis won't. To quibble with "none of these are acceptable in Agda": it seems unlikely that Agda or anything like it would detect hangs or timeouts due to code not meeting its deadline. Deadlines and performance constraints are not part of any type system I've ever heard of. Furthermore, performance is dependent on the compile toolchain, the runtime, and what else is running on the same machine, so it's not even well-defined for static analysis unless you make a bunch of deployment-specific assumptions. A language may guarantee that a function is total in a theoretical sense, but you might not be able to calculate its value for some inputs in practice. (Consider something like "a ↑↑↑ b".) So this guarantee is subtly different from what most users of computer systems would actually want. Of course, as a another commenter pointed out, this sort of practical bug-finding is not actually what the termination guarantee is for.

joel_ms 8y ago
> Yes, static analysis is very useful for understanding what the source code will do for inputs you didn't test. Testing is rarely exhaustive. However, testing will find performance issues where static analysis won't. Static analysis is a funny word to use about what Agda does.. Remember, Agda has dependent types, so what you're calling "static anaysis" involves evaluating/executing functions. In fact it needs to be able to evaluate/execute any functions beyond value-level in any imported modules just to be able to parse a sourcefile, due to the presence of mixfix-notation[0] and how it affects typechecking. > Testing is rarely exhaustive. However, testing will find performance issues where static analysis won't. How do you test a function that takes a natural number? Not an unsigned integer, but an actual countably infinite natual number? For every natural number n you test your function with, you can construct a new natural number n+1 which your function is untested for, (literally) ad infinitum. The answer, of course, is mathematical induction[1] and in the case of more general data structures we have the more general structural Induction[2]. But at this point you don't call it testing, you call it proving, and it's this that Agda is aspiring to. > To quibble with "none of these are acceptable in Agda": it seems unlikely that Agda or anything like it would detect hangs or timeouts due to code not meeting its deadline. Yes, your right that actually detecting hangs or timeouts would be difficult or impossible. But that's not what Agda does. Agda only allows functions that the compiler can figure out are total, which can never be all total functions (otherwise we would have a solution to the halting problem I think.) Basically, functions are either (provably total by the compiler) and hence acceptable. In the case of long/diverging computations Agda just has a timeout threshold, where it rejects a function if it takes too long to evaluate it during typechecking. I'm pretty sure that's what would happen if you tried "a ↑↑↑ b". > Of course, as a another commenter pointed out, this sort of practical bug-finding is not actually what the termination guarantee is for. Correct, it's not for bug-finding at all, but rather to keep the type theory/logic sound when using Agda as a proof assistant. Just to be clear: your criticism makes a lot of sense from a software engineering perspective, but considering the general performance characteristics of Agda, and the almost noneexisiting tooling around it, I think we're a couple of years away from "deployment specific assumtions" being something Agda needs to be too concerned about :) [0] You can define a function "if_then_else_" where the underscores represent arguments, so you would use it like this: "if TRUTH_VALUE then TRUE_CONSEQUENCE else FALSE_CONSEQENCE" [1] https://en.wikipedia.org/wiki/Mathematical_induction https://en.wikipedia.org/wiki/Mathematical_induction [2] https://en.wikipedia.org/wiki/Structural_induction https://en.wikipedia.org/wiki/Structural_induction