Has anyone here read Programming in the 1990s or A Logical Approach to Discrete Mathematics? Symbolic computing is a powerful concept. How does one model somet

Has anyone here read Programming in the 1990s or A Logical Approach to Discrete Mathematics? Symbolic computing is a powerful concept. How does one model something simple that we take for granted such as assignment? Here's a hint: look to Liebniz and Tony Hoare. Symbols and syntactic substitution give you powerful abstractions over expressions. Everything in Lisp is an expression. Symbols give you the ability to develop concepts built up from complex expressions. They let you reason about substitution, equivalence, etc. That's the real power: they're a tool that lets you think above the code. And as others have pointed out, Common Lisp is typed. Type-declarations, though optional, are amenable to static analysis. And the interesting thing about Lisp that I haven't explored much yet is the ability to generate a specification in a higher-level language like PVS perhaps and generate the type annotations from that. The implementation would then have to satisfy the annotations in order to validate the program. Nice article. A Gentle Introduction is a neat book.