lua-users home
lua-l archive

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


If one of the verifications is that the verified bytecode terminates, then it is the same, surely.

That's why we need to define what "safe" means here.

On 1 November 2011 15:44, Tony Finch <dot@dotat.at> wrote:
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.

If one of the verifications is that the verified bytecode terminates, then it is the same, surely.T hat's why we need to define what "safe" means here, or we'll be talking about different things.