Hacker News Reader

You're not wrong when it comes to the theoretical, general case. However, you shouldn't forget that in practice, we're not interested in every possible problem instance. A weaker model often allows for better heuristics.

Take SAT solvers, for example. Since propositional logic encoded in CNF is so restrictive, we can find and implement relatively simple heuristics that solve huge, real-world problem instances in a reasonable time. The same propositional formula can also be represented by a C program which is much, much smaller [1], yet the best heuristic to determine whether the C program outputs 1 for any of its possible inputs, might be to run it once for each input combination (which would take longer than the age of the universe for even 10k variables).

[1] "Proof": the CNF is typically generated from a hand-written program in a practical programming language; therefore, the program represents the propositional formula.

> A weaker model often allows for better heuristics.

Do you have any evidence for that? I have not seen this claim made anywhere. The reason is that heuristics apply in cases where the problem at hand can be stated in terms of a lower-complexity problem, and that happens regardless of model. Is there empirical data showing this is happens more often in restricted models? Intuitively, I see no reason why it should.

> Take SAT solvers, for example.

SAT is NP-complete, which is (well, we don't know for sure, but that's the working hypothesis) much easier than even verification of FSMs (PSPACE-complete). We don't have any similar working heuristics for, say, TQBF (PSPACE-complete), and even SAT solvers fail often.

> yet the best heuristic to determine whether the C program outputs 1 for any of its possible inputs, might be to run it once for each input combination (which would take longer than the age of the universe for even 10k variables).

Most autoamtic software verification doesn't work like that at all, but through a process called abstract interpretation which can conservatively project the problem onto a much smaller state space (that is basically one way to look at how type systems work). The beauty of SAT solvers is that they require no such semantic approximations, and appear to work on arbitrarily difficult problems (except when they don't). So far, they work by magic -- we don't know why they're so effective in practice. But the hope of finding such a general algorithm that happens to work on many real-world instances of problems that are at least PSPACE- or 2EXP-hard problems are not great. It all comes down to studying special cases, and I don't see a particularly good reason (and I haven't encountered any research to that effect) for how to make such "good" instances more likely using some restricted language.

> Is there empirical data showing this is happens more often in restricted models?

Are you asking for studies? How would you even rigorously define the hypothesis?

> SAT is NP-complete, which is [...] much easier than even verification of FSMs (PSPACE-complete).

So? How does that invalidate my example?

> The beauty of SAT solvers is that they require no such semantic approximations, and appear to work on arbitrarily difficult problems (except when they don't). So far, they work by magic -- we don't know why they're so effective in practice.

But that's the point! For real-world problem instances, you'll find that automatically SAT solving a CNF model works much better than applying an automatic theorem prover to the C program that generated the CNF model. That's because in practice, it's easier to design heuristics that work on a propositional formula than it is to design heuristics that work on CNF-generating C programs. If that were not true, then we wouldn't need SAT solver – we'd just run the automatic theorem provers on the C programs that generate the CNF model.

> I don't see a particularly good reason (and I haven't encountered any research to that effect) for how to make such "good" instances more likely using some restricted language.

And yet it works extremely well in the case of the CNF-generating program vs. SAT solving the generated CNF model. That is a pretty strong argument, you cannot just dismiss it because PSPACE harder then NP.

> Are you asking for studies? How would you even rigorously define the hypothesis?

Preferably studies, but even intuition would do at this point. You don't need to rigorously define the hypothesis, just demonstrate which kinds of patterns susceptible to commonly applied automated reasoning occur more frequently when the same application is written in a TC or non-TC language. The thing is that it's often easy to recognize special cases even in TC languages (e.g., deducing that a function is total in a TC language is easy in those cases where the function resembles those used in non-TC languages).

I'm not saying languages can't make verification easier. For example, recognizing a terminating loop may be a bit easier in a language with `for` loops than in a language that only has a `goto` construct, and a language with less/no aliasing makes local reasoning much easier; I'm saying that that help does not stem from restricting the computational model (just as removing `goto` does not reduce the computational power). Turing-completeness in itself is a red herring when it comes to the question of how languages can help verification.

But I don't understand even the general line of your argument. Even supposing that SATing a CNF formula automatically generated from C is easier than other approaches (it isn't), this does not show that writing CNF directly is more advantageous than writing C. After all, a simple mechanical translation exists, so why should I write CNF formulas if writing equivalent C code is easier?

> you'll find that automatically SAT solving a CNF model works much better than applying an automatic theorem prover to the C program that generated the CNF model.

It doesn't, though. Many automatic problems are easier to verify using abstract interpretation than SMT.

> So? How does that invalidate my example?

That a magical 50-year-old algorithm that no one understands to this day happens to exist for the very simplest of intractable problems does not mean that we can hope for similar success for much, much harder problems. When it comes to program verification, SAT (used in SMT) is effective only in a very controlled and limited way (I know because I use formal verification). No one believes SMT solvers could be extended to verify full programs.

> but even intuition would do at this point.

Maybe this example helps: I should be easier to write analysis heuristics for a language that only allows loops of the form "for i = 1...n" than for one which also has while-loops, gotos, and unrestricted C-style loops. Maybe not from a theoretical point of view – after all, both languages are equally Turing-complete – but from a practical one, since there are more language constructs that have to be covered by the analysis. Sure, you can mechanically translate all loops from the second language to "for i = 1...n" loops, but that transformation is not trivial and has to be implemented first.

> But I don't understand even the general line of your argument. Even supposing that SATing a CNF formula automatically generated from C is easier than other approaches (it isn't), this does not show that writing CNF directly is more advantageous than writing C. After all, a simple mechanical translation exists, so why should I write CNF formulas if writing equivalent C code is easier?

My point isn't that we should hand-write CNF formulas. What I'm saying is, that automatically solving CNF formulas is easier than automatically solving a C program that expresses the same thing.

Example: a Sudoku solver. Given a partially filled 9x9 matrix,

* ) Program 1 takes as input an assignment for the unfilled fields (free variables). It outputs yes/no indicating whether the input satisfies the Sudoku rules.

* ) Program 2 generates a CNF instance which encodes the Sudoku rules and the partially filled matrix. The variables represent the unfilled fields.

Program 1 and the output of program 2 are equivalent in the sense that they encode the same problem instance, but the CNF generated by program 2 is in a much more restricted language than program 1. You can write a decent (although not state-of-the-art) CNF parser and SAT solver in a few 100 lines of code, but you will be hard-pressed to write even the parser for a general C program in that space, let alone something that can understand C's semantics, an automatic solver using abstract interpretation, and some heuristics to speed things up (only those heuristics are allowed to be somewhat tailored to this type of problem, everything else has to be general-purpose – just like the SAT solver, which is general purpose and has a few heuristics that speed up many practical instances).

> It should be easier to write analysis heuristics for a language that

Quite possibly, and that's exactly what I said. Languages may assist formal reasoning (although how is not always clear[1] and your example may or may not be valid -- the transformation in the well-behaved cases may be quite easy; compilers and static analyzers do such analysis all the time), but that's not due to a weakening of the computational model.

> What I'm saying is, that automatically solving CNF formulas is easier than automatically solving a C program that expresses the same thing.

Right, but as the transformation is mechanical, there is no reason to prefer one language over the other. They're equivalent -- in this particular scenario -- from both a theoretical and a practical point of view. Static analyzers commonly perform transformations -- from the programming language to SMT-LIB and/or using abstract interpretation.

> but you will be hard-pressed to write even the parser for a general C program in that space

Writing a compiler for Pascal is much harder than writing an assembler. That's not an argument for writing assembly by hand over writing Pascal.

[1]: One example is a pure-functional language like Haskell vs. an imperative one like Java. Well-behaved Haskell allows for equational reasoning while Java "only" allows for assertional reasoning, but the common use of higher-order functions makes some automatic reasoning methods much harder than the familiar and powerful assertional reasoning approaches.

> 2. that does not mean that reasoning in weaker models is feasible.

If you limit it explicitly to models powerful enough to run arbitrary computation, then that sounds reasonable.

But there are a whole lot of situations where a sufficient set of useful algorithms for that given context are computable using models that we can reason much better about if you are willing to throw out the requirement to be able to run arbitrary computations.

A simple example is that you can easily define a model of computation that "solves" the halting problem the crude way: Just add an upper bound to the number of steps, and halt the problem after that number of steps. Now you know any program halts. Make the limit low enough and it actually makes a difference. Of course this model can not compute arbitrary programs. But depending on your needs it may be able to compute sufficiently complex programs.

More reasonable examples would be specialized domain languages like Sieve for filtering e-mail, that address reasoning by having no branching or loops or writable state.

The challenge is that accidentally expanding such a model in ways that accidentally adds back enough power to cause problems in reasoning about the programs is very easy.

> But there are a whole lot of situations where a sufficient set of useful algorithms for that given context are computable using models that we can reason much better about if you are willing to throw out the requirement to be able to run arbitrary computations.

This is not true, and precisely the point of my comment. There are no computational models of any wide utility -- no matter how limited -- that we can feasibly reason about in the general case. When I said "arbitrary" I meant arbitrary in whatever restricted model you give me. We can reason about many special cases, but we can (and do) do that for Turing complete languages, too.

> Make the limit low enough and it actually makes a difference. Of course this model can not compute arbitrary programs. But depending on your needs it may be able to compute sufficiently complex programs.

Again, this is not true. Knowing that your algorithm is bounded by some number, gives you no additional information usable in verifying it. There is still no faster way of answering questions than running the program on all inputs up to that number.

> that address reasoning by having no branching or loops or writable state.

If you have no loops (even bounded by a depth of 2) and no subroutines or no variables -- then verification is feasible, otherwise it is at least PSPACE-hard. Such languages may be useful for something, but obviously the vast majority of tasks cannot be done in them.

> The challenge is that accidentally expanding such a model in ways that accidentally adds back enough power to cause problems in reasoning about the programs is very easy.

This is provably impossible unless your don't mind your programs being as long as the worst-case time complexity that they solve. For almost any computational model (barring a couple of very special exceptions), the verification complexity is θ(|S|). As we know the minimum number of states for algorithms, the verification cost is known. The only thing you can do is make the languages so inexpressive that programs increase polynomially or exponentially in size, and so the verification complexity would decrease.

In general, the idea that a weaker computational model makes reasoning easy is a myth (obviously not one shared among researchers). The myth is probably because many practitioners know about the halting theorem but not about more significant computational complexity results, and mistakenly believe that it is that result which is the cause of the difficulty of verification.

> There are no computational models of any wide utility -- no matter how limited -- that we can feasibly reason about in the general case.

I gave you an example: Sieve.

> If you have no loops (even bounded by a depth of 2) and no subroutines or no variables -- then verification is feasible, otherwise it is at least PSPACE-hard. Such languages may be useful for something, but obviously the vast majority of tasks cannot be done in them.

Sieve, as I mentioned fits in this category (though I'd not be surprised if there are extensions that break this; there are many, but the basic language is sufficiently constrained and still useful).

The point is not to do "the vast majority of tasks" in them, but that a wide range of tasks are constrained enough to achievable within different sets of such models, and this is a common way of seeking to contain computational complexity that works well when it is done by care.

(... but leads to unexpected Turing completeness now and again when people don't take care, as the article points out)

E.g. aforementioned Sieve is constrained this way explicitly to be safe to let end-users -- or scripts on their behalf -- construct Sieve filters to run during delivery on mail servers without e.g. having to impose any other restrictions than a size limit.

> This is provably impossible unless your don't mind your programs being as long as the worst-case time complexity that they solve.

I think you misunderstood what I wrote. The sentence you quoted here is arguing that people make mistakes when defining the kind of restricted languages I'm discussing all the time so that verification gets harder. You seem to think it was talking about making verification easier.

> In general, the idea that a weaker computational model makes reasoning easy is a myth

And again: This is flat out wrong without adding the caveat that you're talking about arbitrary computation rather than languages that are specifically and intentionally constructed to prevent arbitrary computation.

Here's one:

    Consider a machine whose only instruction is "halt", which halts execution.

Clearly this model is trivial to reason about. You may intend a "useful" in there somewhere, in which case I point you again to Sieve, which is still trivial enough unless you carelessly add extensions.

> I gave you an example: Sieve.

I said "of wide utility". BTW, I don't know Sieve, but if it has regular expressions then reasoning about it is also infeasible (e.g. checking whether two filters based on regular expressions are equivalent).

> but that a wide range of tasks are constrained enough to achievable within different sets of such models, and this is a common way of seeking to contain computational complexity that works well when it is done by care.

I don't know what "a wide range of tasks" means, but even regular expressions are not limited enough for general reasoning. Anything that requires regular expressions and beyond is already infeasibly verified in the general case.

> This is flat out wrong without adding the caveat that you're talking about arbitrary computation rather than languages that are specifically and intentionally constructed to prevent arbitrary computation.

No. I'm talking about arbitrary programs in whatever language you give me. If your language has regular expressions -- game over. If it has variables and subroutines/limited loops -- game over. And those are just the PSPACE-hard cases. If all you have in your language is boolean connectives (i.e., it's a propositional calculus) -- no subroutines, no loops and no mutable variables -- verifying it is "just" NP-hard. Special cases, on the other hand, are often possible to reason about even automatically even in Turing complete languages.

> You may intend a "useful" in there somewhere, in which case I point you again to Sieve, which is still trivial enough unless you carelessly add extensions.

I did say useful, and either Sieve is not very widely applicable and/or, if it has regular expressions it cannot be feasibly reasoned about.

> I said "of wide utility".

And they are of wide utility, even though they may not satisfy your expectations to just how wide utility you want. But that is exactly the point - they're not meant to.

The claim I made, and that others here have made, that you've been arguing against is not about general purpose languages. I've pointed that out several times.

On the contrary the point is explicitly that there are benefits in isolating parts of problems and explicitly avoiding general purpose languages exactly because I agree that you won't gain much from trying to find weaker models for general purpose languages.

So when you keep bringing up more general computation, you keep arguing against a point I at least have not made.

I've never disputed that there is little to gain from trying to weaken the computational models for general purpose computation.

What we can do, and often do is to reduce the practical problems of working on these systems by lifting subsets of problems out of general purpose languages and into much weaker special purpose environments.

Since you keep bringing up regular expressions, for example:

> but if it has regular expressions then reasoning about it is also infeasible

... this is exactly one of the reasons why Sieve doesn't have them (at least not the base language) - it's limited to basic wildcards ("","?", specific strings). On top of that the implementation is allowed to terminate execution after an implementation defined number of execution steps, so it does not need to even deal with the worst case for a wildcard engine if someone tries to feed it pathological strings.

> I don't know what "a wide range of tasks" means, but even regular expressions are not limited enough for general reasoning. Anything that requires regular expressions and beyond is already infeasibly verified in the general case.

I've repeatedly pointed out that the entire goal of these languages is to prevent* general reasoning. That is a feature, not a flaw.

> No. I'm talking about arbitrary programs in whatever language you give me.

... in which case you're not addressing the comments of mine that you've replied to, and we're in violent agreement about something that is irrelevant to my argument.

> What we can do, and often do is to reduce the practical problems of working on these systems by lifting subsets of problems out of general purpose languages and into much weaker special purpose environments.

A language that has no variables, no loops and no subroutines (and no regexps) is as far as you can go while remaining feasibly verifiable. There aren't many other options. What portion of our applications can be written in such languages? That people add extensions to Sieve only shows that its trusted portion isn't widely-enough useful even for the task of filtering email.

It's not a question of general-purpose vs. DSL. Regardless of what the language is for, with no loop, subroutines and variables there is very little you can do.

> I've repeatedly pointed out that the entire goal of these languages is to prevent* general reasoning. That is a feature, not a flaw.

It's not important, but that's not what I meant by general reasoning or arbitrary computation. What I meant is that no matter the language you give me (assuming it's useful enough etc.), answering arbitrary questions about arbitrary programs in that language is not feasible. For example, regular expressions do not allow "arbitrary computation" in the Turing completeness sense, yet it is infeasible to feasibly answer arbitrary questions about arbitrary regular expressions, such as the question "are two regular expressions equivalent?" This is a very important question about regular expressions, but it cannot be feasibly answered for arbitrary regular expressions.

> A language that has no variables, no loops and no subroutines (and no regexps) is as far as you can go while remaining feasibly verifiable. There aren't many other options. What portion of our applications can be written in such languages? That people add extensions to Sieve only shows that its trusted portion isn't widely-enough useful even for the task of filtering email.

Most extensions to Sieve still retain the same constraints. A few don't, sometimes because peoples needs are different: E.g. someone using it for their own mail server or a corporate mail server where it is possible to yell at the person who turned their mail script into a fork bomb has very different requirements from one that lets "anyone" sign up, for example. That's a good reason for why the extension mechanism is there.

As for examples of other things you can do: There are a number of templating languages, for example, that can be demonstrated to always terminate and otherwise be feasible to reason about. I've personally written such template engines also because it was a useful way of preventing the developers from doing stupid things (the ingrates then tried to sneak in a directive to embed a perl interpreter behind my back at one point).

You can do a lot more than you might think in such engines by e.g. providing primitives for filtering and iteration over nodes in input graphs (as long as you can't mutate the collections, and there are appropriate termination guarantees e.g. by preventing loops)

Another highly useful example that springs to mind is BPF, which while it started as a basic packet filter (e.g. for tcpdump) is increasingly powering much more functionality on Linux for e.g. tracing, and such as for example kernel level enforcement of system call constraints (you can define filters to apply to subsequent code that e.g. outright rejects certain system calls, or applies comparisons to the system call arguments to decide whether to allow or reject them).

But I'd say the question you're asking is the wrong one, though. The original point was that when approaching a problem, there is substantial value to be had by asking "how can I subdivide this problem so that as much as possible can be restricted to a less powerful subset?" The Rule of Least Power, basically.

Often you will end up with dynamic subsets that are hard to reason about, but as part of the process you can usually confine the parts that are hard to reason about to a smaller portion of the code and reduce the magnitude of the problem, and gain the ability to reason about the rest.

You don't even need to create full blown languages to get this effect - changing the way you write code and effectively create a DSL in the form of API's can often achieve the same effect, but isolating "dangerous" functionality to separate languages often makes it harder to violate the requirements.

> It's not important, but that's not what I meant by general reasoning or arbitrary computation. What I meant is that no matter the language you give me (assuming it's useful enough etc.), answering arbitrary questions about arbitrary programs in that language is not feasible

That'd be reasonable apart for setting it up for a No True Scotsman with your "assuming it's useful enough etc.". As we've seen with your objections to Sieve, the languages I'm talking about appears to be languages you don't find "useful enough." Since your objections applies to a different set of languages than those I'm talking about, your objections are moot.

> as part of the process you can usually confine the parts that are hard to reason about to a smaller portion of the code and reduce the magnitude of the problem, and gain the ability to reason about the rest.

Alas, this was proven wrong for verification in 2005. See https://pron.github.io/posts/correctness-and-complexity#corr...

> Since your objections applies to a different set of languages than those I'm talking about, your objections are moot.

1. I reject your examples on the ground that they're considered insufficient for their own domains, and in any case are so restricted that you could not compose the lion share of an application from them even without the theorem showing that you cannot reduce the cost of composition by verifying simple components.

2. While I'm happy to further ponder the utility of the languages you listed, you should bear in mind that, say, a Java program using similar constructs to a Sieve program can be reasoned about automatically by current tools, and with relative ease. In other words, a program so simple is easy to reason about whether it's written in a restricted or a non-restricted language, so using those DSLs just increases the cost of verification. However, that does not mean they are not useful. For example, I read that the main design object of Sieve is to allow servers to run untrusted code.

Practitioners are usually concerned about what is true in practice. Weaker computational models have found great success in databases and parallel programming (e.g. Googles MapReduce) because they are easier, in practice, to reason about and optimise.

> Weaker computational models have found great success in databases and parallel programming (e.g. Googles MapReduce) because they are easier, in practice, to reason about and optimise.

Most SQL variants [1] and map-reduce [2] are Turing complete. They are easier to optimize in practice because they tend to be small and simple (compilers often make similar optimizations for similarly-sized general purpose programs) and because they express the parts that are important to optimize for that particular problem (data-dependence and parallelism) in a direct way -- not because of the computational model.

You could argue that because SQL is cumbersome for general-purpose programming it helps ensure programs are small and simple, but most people would rather not write their application in SQL, and if they did, it would no longer be small and simple.

[1]: https://stackoverflow.com/questions/900055/is-sql-or-even-ts...

[2]: https://www.quora.com/Theoretically-can-any-algorithm-be-imp...

SQL Turing completeness is generally regarded as a (relatively recent) mistake. MapReduce is only regarded as Turing complete as it is typically programmed using Turing complete languages. In both cases, the validity of many optimisations would be destroyed by any non-terminating behaviour. You could have a situation where a query's termination depends on the optimisations used. IMHO, this is highly undesirable.

Perhaps a better example is the humble Regex. If we have a true regular language, we can optimise it via a DFA to have O(N) runtime. The weak computational model is enabling this optimisation.

> You could have a situation where a query's termination depends on the optimisations used. IMHO, this is highly undesirable.

Termination and exponential (or super-exponential) running times are about equally bad. Avoiding either is done on a case-by-case basis. Restricting the language can save you from one and not the other.

> If we have a true regular language, we can optimise it via a DFA to have O(N) runtime. The weak computational model is enabling this optimisation.

I'm not an expert on regex by any means, but I believe this optimization is exponential (a DFA can be exponential in the size of the regex), and so infeasible in practice. Regardless, as I said, regex is about as far down as we can take computation, and regexps make for a very poor generally useful computational construct.