&gt; An example of &#x27;unreal&#x27; code would be me spending a weekend trying to write Goodstein&#x27;s Theorem in Coq. &#x27;Real&#x27; code would be a web app written in Perl.<p>I doubt that &quot;web app written in Perl&quot; will be a realistic target for provably-correct code in, say, the next decade. It&#x27;s much more likely that, as the cost of verification decreases, critical <i>components</i> will start becoming verified. For example, the core routines of encryption libraries, network schedulers, payment systems, etc.<p>Even so, some properties (e.g. memory safety) can be proven at the language level. That way, by verifying a Perl interpreter, we automatically verify every &quot;web app written in Perl&quot; for free ;)