Oh one last thing I forgot to add is that since we want this low-level / high-level consensus / non-consensus language split regardless, the details of the low-level language become somewhat less important. i.e. with some effort your high level BTC lisp language could probably be translated/complied to Simplicity using this “values computed from an environment are just functions” interpretation, at least modulo issues of unbounded-recrusion and choice of primitives. Similarly, wherever the design of Simphony ends up, it can probably be translated/complied your low level btc lisp language, with each translator/compiler language pair offering different potential complexity/optimization opportunities.