9 ms·

>It is possible to formally prove things about programs in Turing-complete languages. But not about arbitrary programs you download from the Internet. For such

by zeteo 15y ago

>It is possible to formally prove things about programs in Turing-complete languages. But not about arbitrary programs you download from the Internet. For such programs you need to require either that they include a custom proof, or that they're written in a non-Turing complete language so that you can check safety yourself.

gbhn 15y ago
... or you could adopt a personal policy of just not running such programs. That's the top-level poster's point -- the boundary between statically-analyzable and not is extremely complex, and not coincident with Turing-completeness.