A "toothbrush" utility Matt Kaufmann ACL2 Seminar, 11/18/2014 This talk will present a "toothbrush" utility for creating ACL2 applications that depend on only a small(-ish) fraction of the ACL2 source code. Warren Hunt wanted this utility in order to create ACL2 applications with a smaller memory footprint than they would have simply by starting ACL2, loading the application, and then using save-exec to save an executable. The "toothbrush" name was bandied around in the early 1990s at Computational Logic, Inc., the idea being that you don't want to load all of ACL2 merely to run a toothbrush. After I go briefly through books/system/toothbrush/README, the talk will consist of two parts: - A demo will show how to use this utility. - We'll walk through the "toothbrush" source code, which I think could be useful to those who want to do ACL2 programming.