|
|
|---|
|
|
|
|---|
ATC tutorial: Motivation for Generating C Code from ACL2.
(This page may be skipped at first reading.)
The motivation for generating C code from ACL2 is analogous to the motivation for generating Java code from ACL2, or for generating code in other programming language from ACL2. The java::atj-tutorial-motivation page provides the general motivation, in the context of Java: it is recommended to read that page.
In addition, as a specific motivation for generating C code, it should be noted that C is widely used in certain domains, such as embedded systems and device drivers. Some of these C applications are relatively small in size and have strong safety and security requirements, making them an attractive target for (ACL2-based) formal methods.