2

I have read a recent article about juvix optimizations to adjust for michelson specifics

https://research.metastate.dev/juvix-compiling-juvix-to-michelson/

And saw that michelson has 2 features mentionned there that can make its execution costly in terms of gas

1) Michelson has no concept of a heap

2) Michelson is a stack machine with an inefficient lambda

So my questions are:

  • What are the design considerations in a blockchain context that make those 2 features necessary ?

  • would changing 1 or 2 go in the way of formal verification ?

2
  1. Having a heap in your language is slightly more powerful and simpler for compilers but this effectively increase the number of instructions and the burden on formal verification. For example, it's not obvious how, in a simple enough manner, to introduce heaps and keep the current GADT in the Michelson interpreter.
  2. Inefficient lambdas directly come from having only one argument in lambdas. This forces lambdas to take pairs (or pairs of pairs, or combs, etc.) which means creating them is cumbersome and a bit costly at execution. This is again linked to typing / the GADT. However, this one is probably relatively easy to improve in a next proposal and is already discussed among core devs.
| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.