The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  I admit this question is "soft" in that there isn't a correct hard answer. tinstrDenote seems a bit too magical to me, and I would like to understand its limitations. If I am using the wrong terms / should re-read some section, please let me know.

================ Context =================

I'm reading Chapter 2 of CPDT.

tinstrDenote feels a bit too magical to me, especially the part about:

  1) statically know the # of elements on the stack

  2) statically know the type of the elements on the stack

This seems like it solves all problems in formal verification and I'm trying to understand why tinstrDenote does NOT solve all problems.

instrDenote: http://adam.chlipala.net/cpdt/html/StackMachine.html#instrDenote

tinstrDenote: http://adam.chlipala.net/cpdt/html/StackMachine.html#tinstrDenote

I'm trying to understand why this works -- and I think the magical part is here:

https://gist.github.com/anonymous/ac0a2dc3c519c0557f8e

Now, I can believe this works since (s: vstack ts) captures the # of elements and the type of elements in "ts".

========== Below this is my confusion ===============

It seems important that all programs in chapter 2 always execute a _constant_ number of steps. Thus, it's as if it's proving:

for every k,

  for programs who execute at exactly k steps, regardless of it's input, we can show that it's type safe / doesn't stack underflow

  so one function we could encode would be something like f(x) = (x + 2) * 5 + 100

  now, f(2) and f(100) both take the same # of steps, and have the same intermediate "type stack"

Here is my confusion: suppose we were dealing with programs whose # of steps (though provably finite), depended on its input; say f(x) takes x^2 steps.

Is this where "direct application" of chapter 2 falls apart? In order to prove type-safety of a function f(x) that takes x^2 time, we need to find invariants / induct. This inturn, requires human insight / intuition / things crush can't brute force -- and we end up returning to a manual process.

Thanks!