> All you have to do is demonstrate that TMs can be simulated in JavaScript, and that's fairly easy to do since TMs are so bare-bones.
Actually I think this is fairly non-trivial. Sure you could make a "compiler" that compiles a JavaScript interpreter down to a Turing machine, but you would almost certainly not understand the generated states and transitions.
A more elegant model of computation is the lambda calculus. It's also very bare-bones, but it's easy to imagine writing real programs in it. Functional programming languages, at their core, are just lambda calculi with some syntactic sugar.
It's practical, but it's also a good foundational model. It's easy to reason about, due in part to the fact that it models familiar math (partial functions).
There are far simpler models for formal verification than Turing machines, e.g. Smullyan's top-down tableaux method - you make a simple functional snippet and immediately verify it using mostly general induction and easy-to-understand verification steps that can be almost automated. Going all the way to the Turing level would kill you time-wise to get to anything useful (even preparing description of your JavaScript machine in Turing terms) - Turing machine has infinite time available, you don't.
Not to mention there are some issues with formal logic that might cause you problems (hint: why do medical doctors use counter-factuals and not mathematical logic?)
"Beware of bugs in the above code; I have only proved it correct, not tried it" -- Donald E. Knuth
