Clarify the workflow of Proof Carrying Code

[andrew-johnson-4]

Based on my own experience and theory of how this should work, strongly verifiable code happens in three separate steps.

1. Code is written to implement some core functionality
   • this code may be slightly fragile or even buggy
   • changing requirements make it hard to maintain this code without introducing bugs
2. Global rules (usually just best practices) are created to tame the bugs
   • in proof carrying code, these are actual verifiable assertions
   • i.e. double free will never happen
3. Original Code is annotated with type hints to prove that it satisfies the global rules
   • this process greatly strengthens the original code
   • it is now easier to make changes to original code without worrying about unintended consequences