OCaml comes to mind as a static language with a macro system that sees a lot of use. I have no idea, though, how sound its type system is. For my part, my sens

OCaml comes to mind as a static language with a macro system that sees a lot of use. I have no idea, though, how sound its type system is. For my part, my sense is that it would be appropriate for a static lisp to choose completeness over soundness in its type system. Gödel's incompleteness theorem tells us that a static type checker can't be both sound and complete. So you've got to pick one, and there's something about sacrificing liberty for the sake of security that strikes me as being fundamentally un-lispy. All the talk further up about CL-style unhygienic macros seems like a good illustration of the relevant culture. You can't ignore Scheme and Racket, of course, but the longer tradition in Lisp is to say, "We'll give you all the power and all the footguns, and leave it up to you to use them responsibly."