This looks like a cool project. It looks like it is up to the host language to compile to bytecode and do all the type analysis before passing that info to the verifier. Looks like there is no VM yet, it just verifies the bytecode and then prints it. But it looks like the host language must also be written in Rust because the main `go` method is expecting rust types. Is that correct?