> An example of 'unreal' code would be me spending a weekend trying to write Goodstein's Theorem in Coq. 'Real' code would be a web app written in Perl.
I doubt that "web app written in Perl" will be a realistic target for provably-correct code in, say, the next decade. It's much more likely that, as the cost of verification decreases, critical components will start becoming verified. For example, the core routines of encryption libraries, network schedulers, payment systems, etc.
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 "web app written in Perl" for free ;)
I doubt that "web app written in Perl" will be a realistic target for provably-correct code in, say, the next decade. It's much more likely that, as the cost of verification decreases, critical components will start becoming verified. For example, the core routines of encryption libraries, network schedulers, payment systems, etc.
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 "web app written in Perl" for free ;)