What are some similar projects?
The entire Verified Software “Grand Challenge” work is related, and in fact, I believe that the idea of “open proofs” is a complement to the “grand challenge” work. The “grand challenge” work wants to create proofs of larger systems, but it fails to make clear what people will be allowed to do with the works once they are created (at great expense). Wheeler thinks this is a terrible mistake; creators should never start developing software or evidence until they know how it will be released. If the license of verified software prevents building on it, then there is a very high risk that all that money and effort will be wasted. Thus, “open proofs” can be considered a practical strategy for implementing the verified software grand challenge, by eliminating legal roadblocks to implementing and using the results of the verified software grand challenge.
