> ...existing uses of Iris perform the proofs "on the side" using transcribed syntax tree versions of the target code rather than directly reading the original source.
I'm a formal verification dummy, so can someone please confirm if this means these uses of Iris are creating an Abstract Syntax Tree (AST) of the source, then operating upon that AST?
If so, can I please get an ELI5 why there is a salient formal verification outcomes difference between using the AST and "directly reading the original source"?
I'm a formal verification dummy, so can someone please confirm if this means these uses of Iris are creating an Abstract Syntax Tree (AST) of the source, then operating upon that AST?
If so, can I please get an ELI5 why there is a salient formal verification outcomes difference between using the AST and "directly reading the original source"?