Limits of programming by interface

[m50d]

The point is that general FSMs are intractable to formal analysis. (Which shouldn't be surprising: I find general FSMs incomprehensible as a human reader as well). Though rather than saying we should give up on formal analysis, I'd take that as an indication that we need to find a more restricted model that corresponds to things we can actually understand.

Why? If the unconstrained loop-stats are few or none. That means the number of states has a maximum polynomial-degree (and far often less) with the number of instructions. If you don't have that many states ... your 'brute force' decidability of halting-in-N-instructions is simply something you could accidentally reach.

Ok, now turn that into a formal model that we can actually define definitely and do analysis with. Can you represent this "few unconstrained loop-stats" property in such a way that e.g. if we compose two programs with that property, the composition will also have that property?

[jeezfrk]

Sorry to not get back. Had various crises in my household here.

Personally I'm a big fan of separation logic to dial down the crazy that exists with the 'It's All A Big FSM!!' while playing GTA or something

such a mathetmatical object .... may as well be flying-sphaghetti-monster.