ACL2 is a mathematical logic, programming language, and mechanical theorem prover based on the applicative subset of Common Lisp. It is an "industrial-strength" version of the NQTHM or Boyer/Moore theorem prover, and has been used for the formal verification of commercial microprocessors, the Java Virtual Machine, interesting algorithms, and so forth.
Re: Why such an IMHO offensive name?
> do you guys want to popularize on
> Franz's success? Or is it a bad pun on
I doubt there was any intended connection. Franz's renamed their product from "ExCL" to "Allegro CL" in 1988 (according to their company history page), and the ACL2 project began in 1989 (according to their acknowledgements page).
Re: Configuration made simple...
Things like your "type" and "unit" and "description" should not be in the config file. The actual config file itself should look something like this:
Whereas things like type, unit, descrption, etc. should live in a configuration description file which sets up what valid parameters are and form the basis for UIs.
This keeps the config file itself simple, while maintaining all your data.