I have read a recent article about juvix optimizations to adjust for michelson specifics
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 ?