The language design, that on EVM v.s. that on Others

I am analyzing a compiler which was called Bamboo Compiler.

For me, the design was something unreadable and it was an incomplete model as an escrow language.

Now, I clean up and aliasing the former work and I put it on my github as pen compiler project.

Loops and Program Graph

Bamboo does not have loops in the language design, claiming that we do not need loops because we have gas limit in the execution.
I think this is not the word of those who create a User Friendly Language.
The dijkstra’s Guarded Command Language(GCL) is a way of defining formal method and solving this kind of problems. GCL is translated into Program Graphs easily.

It is compiler that transform loops into a safe finite sequences of opcodes.

This might allow us to use loops in the language design.

Functional OOP

Unlike Bamboo, I would like the approach of Functional OOP language design which is developped by B.C. Pierce and so on around 90’s, which is the original model of Objective Caml.
I heard that Bamboo cannot fill the gap between escrow language which @pirapira pursued and the EVM design which is quite similar to OOP design.

I would like to see and borrow ideas from a lot of projects now going , e.g. michelson in Tezos.

I found Bamboo compiler lacks some of EVM opcodes like CALLCODE which I believe caused the parity bug. I do not know now, how to avoid this operation called from some sender, and in the design of Functional OOP. The first thing is to do the whole design of FOOP on EVM roughly.

Stack Verification

Recently, a team on tezos language developped a formal way to anlayze the language in order to grasp if the language terminates as intended.
This is done by applying Refinement Type to the Stack. Refinement Type can have a “predicate” on every Type. We can have every subset of every type as a set with applying the predicate.
Thus, type checking on the type of stack contents is exactly formal vericafition of the program.
( However, this type checking sometimes does not terminate if it has second-order logic. )
The implementation depends on SMT solver for the computation of the logical part.

I would like to try this on EVM.

TODO

  • make Guarded Command Langauge for EVM
  • define Functional OOP
  • add stack verification

I would like to know much more about language designs.
If anyone know about them or interested in them, feel free to let me know !

There are bunches of unneeded definitions / corrupted designing in Bamboo

  • Interface Types do nothing / have no meanings in Bamboo.
  • Multiple Returning do nothing in Bamboo…
  • Void Type and Empty List has the same Role in Bamboo.
  • Bamboo’s case is not case pattern match.
  • Sentence was Just a Statement
  • append_label has a different role from appending labels
  • duplication of functions which does the totally same role
  • Bamboo has two different names for functions, cases and functions.
  • The term interface has multiple meanings in Bamboo Compiler

The design of Bamboo seems fully unreadable and full of useless designs.
An ordinal type theorist would not write codes in such a way.
Pen is going to be a much simplified and sophisticated version.
And let’s try to make typed functional programming languages on evm.

The Bamboo Compiler turned out to be a useless compiler in terms of formal verification.
The guard code 'reentrance` in Bamboo does nothing in creating contracts.
Unlike, type checking in a single computer which has a single user, EVM has bunches of users who use the function. Thus outside checking process does not guarantee the safety. Rather, we must have the guard condition inside the contracts.
I have remembered someone pointed out the uselessness.

It’s just a compiler.
There is no formality on it.
Thus, that means pen also has no formalities in terms of contract safety checking.
We have to make them from the bottom.