The proof will be more friendly to nowadays programmers if we treat all "Gödel numbers" as bytecode of a programming language. It's trivial that functions like "prove" and "subst" can be implemented based on abilities like bytecode parsing and expression tree manipulation.