If you want to prove that a complicated function which contains a forbidden line will ever actually execute that line given any input, then yes, the turing-comp

If you want to prove that a complicated function which contains a forbidden line will ever actually execute that line given any input, then yes, the turing-completeness of Javascript makes it difficult to prove that the function is safe, because you can't even prove that it will ever halt, let alone reach a line. But imagine that Javascript were simpler--say, it could only contain the control flow constructs if, !, &&, ||. Then, in order to prove that a complicated function never reaches a forbidden line, you have to solve a 3-SAT problem, which is NP-complete and also impractical to prove for all functions. The only sure way to prove that a function is safe, turing-complete or not, is to restrict the system calls it can make. I agree that if you provide domain-specific non-turing complete languages, it's more likely that you will be able to grok it and pull it apart, but it doesn't let you prove that any arbitrary function doesn't reach a line you don't like for all user input.