programming languages with formal verification systems backed by state-of-the-art theorem provers
Ah so Vitalik does realize there is a problem like the sort I am pointing out. But perhaps he has not yet realized that even 100% dependently typed scripting won't fix
the problem I am claiming is inherently insoluble.
I would like to hear comments from Vitalik on this. I have not seem him answer these questions directly.