Technical details how Kindelia makes deploying formally verified apps economically viable?

[lancejpollard]

I am reading again through the whitepaper and formulating some questions. I don't know much but I have some experience with Coq and the reasons for and benefits of formal verification.

I see this:

Deploying formally verified apps written on these languages to Ethereum or Cardano is not economically viable, but, thanks to HVM's functional opcodes, including constant-cost beta-reduction and pattern matching, Kindelia can handle these natively and cheaply.

I saw the list of 12 opcodes. I am familiar with opcodes from assembly but not in terms of functional languages, I only have very basic knowledge and hello world experience with Haskell. I have read about beta-reduction in type theory but I don't know what it means. Pattern matching I imagine is like from rust, but I don't know how it's typically implemented in a functional language. I also don't know much technical implementation details of Ethereum, which might benefit from more expansion into how the parts work which are relevant to Kindelia.

Given that, can you explain in more technical detail what these components are and how it works to make this stuff economically viable?

Thank you! Looking forward to future discussions!