I came to the same conclusion around 2001 while trying to adapt Cigital's ITS4 static security scanner to Perl, but stopped short of producing a "formal proof" :)