|P is for Practical|
I don't really find "If you don't try to solve the halting problem, then you can parse Perl" to be a "stronger" conclusion than "If you don't do something random, then you can parse Perl", other than, of course, the presence of high-falutin' comp sci lingo in the former.
It is a rather simple fact that you can't reliably parse Perl without running Perl code (arbitrary Perl code). It reminds me of showing my kids a clock face and asking them to list the properties of the numbers on it. They never mention that they are sorted, because that just seems too obvious.
The fact that you can't parse Perl is obvious. Adding useless complication to the conjecture makes it sound more like a rigorous proof, but I don't believe it actually helped your proof.
A proof that you can't parse Perl, is:
The fact that run_some_perl_code() can be any arbitrary Perl code is quite clear. I guess this then boils down to the argument that somehow static analysis could be used to predict the results of run_some_perl_code() without actually running it. But the rand example clearly shows that not to be the case. As does using if @ARGV or if <STDIN> =~ /^y/i or if LWP::Simple::get("http://perlmonks.org/secretAlgorithm.pl") =~ /true/ or if unlink "/etc/passwd" or if find_prime_of_length( ~0 ) % 3 == 1.
Sure, the fact that run_some_perl_code() could be trying to solve the halting problem also demonstrates something. Of course, if I'm writing Perl support for an IDE, I'm not seriously concerned that the declaration of function prototypes is being based on answers to instances of the halting problem, so I'm likely to just dismiss your proof (based on your own reaction to the rand case). I find "You might have to run arbitrary Perl code" to be both a stronger statement of the result and a more interesting and useful one.
I also think there is a flaw in your proof in that it confuses solving the halting problem with running code that may or may not halt. So your conclusion would need to be more like "Here is some code that will either determine that whatever() is nullary or that will never terminate." Since just because the code has been taking 400 years doesn't mean that you can determine that it will never halt, so your code doesn't even have the potential of solving the halting problem.
So the lemma that is needed here is that "Static analysis of a program in a Turing-complete language (along with its 'input') can be insufficient to determine its output". Frankly, this is where it becomes uninteresting to me.
(Minor updates applied during the 15 minutes after first posting.)
In reply to Re^3: Perl Cannot Be Parsed: A Formal Proof (obvious)