> In general, verifying programs is extremely hard, not just because of rice's theorem but because it's so easy to miss a spot, especially for non-trivial bytec

> In general, verifying programs is extremely hard, not just because of rice's theorem but because it's so easy to miss a spot, especially for non-trivial bytecode languages like lua's. Perhaps a dumb question then. Java has famously had a bytecode verifier for decades. Is it the case that: a) bytecode verification is fundamentally easier in statically typed languages or b) it's just as hard for Java, but Java has had decades to work on it and it's still taken a long time to fix all the bugs/security issues.