3 ms·

> 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

by adwn 9y ago

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

pron 9y ago
> 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.

by adwn 9y ago

pron 9y ago

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