> 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

> 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