Co-author here. We're planning to turn this into a series, with additional posts on how symbolic execution works at a lower level, how to present counterexamples to users, and ideas for future programming tools built on symbolic execution.
Does any of this stuff work on Java, Python, or JavaScript? I want to improve the quality of real-world programs written in industry-standard languages.
This "gentle introduction" makes it seem like the first step of the process is "port your app to a homoiconic language," -- or, in other words, "you can prove the correctness of any language you want, as long as it's Haskell or Lisp."
we can map each syntax tree to an interpreter
We can define a data type of expressions in our language, with addition, multiplication, etc.
data Expr = Addition Expr Expr | Multiplication Expr Expr | ...
data Interpreter = ...
interpret :: Expr -> Interpreter
interpret (Addition a b) = (+) <$> interpret a <*> interpret b
interpret (Multiplication a b) = (*) <$> interpret a <*> interpret b