lua-users home
lua-l archive

[Date Prev][Date Next][Thread Prev][Thread Next] [Date Index] [Thread Index]

On Tue, Nov 1, 2011 at 3:44 PM, Tony Finch <> wrote:
> Rob Kendrick <> 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.

Yes, this is a good explanation. Verification is a general safety
check - not a proof of termination.

As I said, with some VMs, bytecode verification is a null operation.
And those VMs are turing-complete too.