The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 06/27/2013 11:58 PM, t x wrote:
> 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.

Here's a concise answer which I hope helps: The two properties you 
mention are decidable.  Most program properties are undecidable.  It 
also helps that the two properties above are _easy_ to decide. :)

> It seems important that all programs in chapter 2 always execute a 
> _constant_ number of steps.

It sounds like this is your intuition behind why the properties above 
are decidable.  I agree with the factual statement, and I agree that it 
suggests a pattern for deciding program behaviors.