[lmm]

To my mind all that says is that even general total languages or finite state machines allow expressing too much. Surely one can solve this by working in a language where functions are not merely total but come with explicit bounds on their runtime. This seems like a good fit for a stratified language design like Noether - we might have to resort to including a few not-provably-bounded total functions (or even not-provably-total functions) in a practical program, but hopefully would be able to minimize this and make the parts where we were making unproven assumptions very explicit.

[pron]

There are languages where all functions run in PTIME (https://www.cs.toronto.edu/~sacook/homepage/ptime.pdf), but this doesn't help.

If your program is a FSM, then your functions run in constant time, and still verification is infeasible. Search for "Just as a quick example of why verifying even FSMs is hard" in my blog post http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...

Languages that are so limited as to be unusable are still PSPACE-complete to verify.

It is simply impossible to create a useful programming language where every program is easily verifiable. Propositional logic -- the simplest possible (and too constrained to be useful) "language" -- is already intractable. Feasible verification in the worst-case and computation of even the most limited kind are simply incompatible. As anyone who has done any sort of formal verification -- it's hard. There are two general ways of getting around this difficulty. Either we verify only crude/local properties using type checking/static analysis (both are basically the same abstract interpretation algorithm), or taylor a verification technique to a small subset of programs. The other option is, of course, to work hard.

[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.