Whats the underlying problem the “open proofs” site is trying to solve?
The problem is that the world depends on having secure, accurate, and reliable software – but the software isn’t. This is especially obvious for security – software we depend on is routinely subverted – so I will focus on that aspect. None of the short and medium term approaches we’ve developed can fully address the need for secure, accurate, and reliable software. In the short term we’re using band-aids like patch distribution systems and firewalls. In the medium term we’ve begun to address the real problem (insecure software) by encouraging the use of tools that search for “likely vulnerabilities” (the webmaster’s flawfinder is one such tool). We’re also doing more testing, which can help, but testing by itself is inadequate because it’s impractical to completely test a program. Completely testing a trivial program that only added three 64-bit numbers (using a trillion superfast computers) would take about 49,700,000,000,000,000,000,000,000,000 years!