[lmm]

> Anything that is Turing-complete cannot be implemented in Ld (by definition). Off the top of my head, this includes: Recurrent Neural Networks, CSS, Minecraft, TrueType fonts, x86 emulators (MOV is Turing-complete) and Conways' Game of Life.

You're begging the question - your Turing-complete algorithm is "evaluate an expression in a Turing-complete language". It's easy to make a language accidentally Turing-complete (especially when you're thinking in a Turing-complete language), but that completeness is undesirable, and in realistic use cases it's harmful rather than helpful. No-one wants to sit waiting indefinitely to see whether a web page or font is actually going to render or not (and indeed we often end up going to great lengths to make these things Turing-incomplete in practice with timeouts and the like).

> No, most algorithms are known to work correctly for the common cases that are tested for + all the edges cases the developers can think of or encounter in real life. For non-trivial software, this is a minuscule subset of the possible states.

You're not contradicting me, you're saying "most algorithms are not known to work". I don't think that's true in the sense of "algorithms" published in journals/textbooks. I would agree that most code isn't known to work, but that translates into reality: most code doesn't work, most programs have cases where they just break and also just crash every so often.

> Lots of things are surprisingly Turing-complete, and it is not trivial to prevent this for a sufficiently complex system.

For a complex system written from scratch, it's easy enough with the right tools. If you build it in a non-Turing-complete language it won't be Turing-complete, and if something is hard to do in a total way it's probably a bad idea.

Porting an existing system would be much harder, I'll agree, and porting the existing code/protocol ecosystem would be a huge ask. (I do think it's necessary though; the impact of malware attacks gets worse every day, the level of bugginess we're used to seeing in software is rapidly ceasing to be good enough).

[pron]

This entire discussion about Turing completeness is completely irrelevant. The problem that's relevant to software verification isn't the halting problem in its original formulation, but a simple corollary of it, often called "bounded halting" (which serves as the core of the time hierarchy theorem, possibly the most important theorem in computer science), which states that you cannot know whether a program halts within n steps in under n steps. The implication is that there can exist no general algorithm for checking a universal property (e.g. the program never crashes on any input) that is more efficient than running the program on every possible input until termination.

But bounded halting holds not only for Turing complete languages, but for total languages, too (using the same proof). In fact, it holds even for finite state machines (with a different proof). This is why even the verification of finite state machines is generally infeasible (or very expensive under restricted conditions) both in theory and in practice.

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