Re: Bytecode: Safe or not? / luac manual

[Tony Finch <dot@...>]

Rob Kendrick <rjek@rjek.com> wrote:
>
> The halting problem is impossible to solve.  A byte code verifier is a
> halting problem.  Thus, a perfect byte code verifier cannot exist.

That isn't true. The proof obligation for safe bytecode is much simpler
than the halting problem, because it only needs to accept bytecode that
can be created by the Lua compiler. It is fine if the checker rejects some
programs that do not crash the interpreter. It is rather like a static
type checker in this respect.

Tony.
-- 
f.anthony.n.finch  <dot@dotat.at>  http://dotat.at/
Fair Isle, Faeroes: Southwest backing southeast 5 to 7, perhaps gale 8 later.
Rough, occasionally very rough. Squally showers. Good, occasionally moderate.