The dynamic nature of #CommonLisp means that reading forms can potentially executing code. So you cannot write a perfectly accurate code analyzer. Or load the code without any side-effect, Erlang style. But I cannot see CL without macros. This annoys me more than it should.
@galdor maybe the situation is less worse: you can write a perfectly accurate code analyzer, but not for all possible #CommonLisp source codes, but only for a subset of them. Maybe, this subset is useful enough. Usually in the final images, all the macro are already expanded, so the analysis can be feasible.
@galdor I never used it, and I don't know how much it fits in this discussion, but today I found this https://www.cs.utexas.edu/users/moore/acl2/
"ACL2 is an interactive system in which you can model digital artifacts and guide the system to mathematical proofs about the behavior of those models. It has been used at such places as AMD, Centaur, IBM, and Rockwell Collins to verify interesting properties of commercial designs. It has been used to verify properties of models of microprocessors, microcode, the Sun Java Virtual Machine, operating system kernels, other verifiers, and interesting algorithms."
@mzan Yeah this is the compromise I have to accept. But to get a reasonable subset, you need a code walker. You can use the SBCL one if you're using SBCL. If not…