Some projects make it possible for you to generate verified code from the specification. There is usefulness to these tools even if the implementation is a sep

Some projects make it possible for you to generate verified code from the specification. There is usefulness to these tools even if the implementation is a separate beast. At a minimum, they allow you to test drive your ideas in particularly thorny areas such as concurrency and security. Forcing you to think hard about a secure kernel or a library of data structures is a good thing in and of itself. You only have to give such core libraries this kind of anal attention, not to the layers built atop.