[lmm]

You're assuming that we can only ever add to languages, not constrain them. Yes if your program has 6 decision points and you model each possible combination explicitly then your model will have 2^6 possible states - but you don't have to model it that way. In previous discussions you've said that humans understand these programs by using symmetries to drastically reduce the size of the state space - let the tool do the same thing.

[pron]

Sure, and model checkers and static analyzers do use symmetries and much more sophisticated ideas (abstract interpretation), but the point remains that it is provably impossible to create a language where every program is feasibly verifiable. My example wasn't even the most restrictive (even though it was too restrictive to be generally useful): it didn't have loops or recursion or higher-order functions. But even a language that doesn't have functions or branching at all, and has only boolean variables is already NP-complete to verify. Computation -- even of the most restrictive kind -- and verification are essentially at odds. In a way, that is the defining feature of computation: a mathematical object constructed of very simple parts, whose composition quickly creates intractability.

On the other hand, specific programs, even in Turing-complete languages, can be feasibly verifiable. We can make our tools more sophisticated, but we can't make our languages restrictive enough that verification would always be possible in practice. There may be things languages can do to help, but changing the expressiveness of the computational model is simply not one of them.

[lmm]

I'm already used to working without unbounded loops and moving away from unrestricted recursion; I can appreciate that unrestricted boolean expressions are complex to verify but I'm just not convinced that day-to-day software development (whether we call it computation or something else) actually needs such things. To my mind verification goes hand-in-hand with implementation, provided the language gives you the tools to do that - maybe I'm arguing for a metalanguage rather than a language, but if I want to produce a program with particular properties that seems easy to achieve by constraining myself to a sublanguage where these properties are true by construction, and then writing my program.