Consider the comparative advantages verification of byte codes over abstract syntax trees.
There is one easy thing that would extend the questionable and precarious advantage that I see to byte codes.
The byte code producer should be required to insert a stack state declaration at each “come-from” point in the code stream.
The producer is clearly in a good position to produce this and with this information the verifier can in a single simple pass can confirm type safety.
No backtracking is required.
At worst the extra work for the stream producer is the same as would have been required by the verifier.
The producer presumably runs less often and with greater computing resources and it is better to move this work from the TCB.
In languages such as JavaScript, without typed variables, a type state declaration for each variable identified in the lexical closure at each come-from point would be required as well.
This change also allows streaming execution as well.