> 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 (a

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