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.

Besides,
as just a compiler,
it does have a fatal bug.
setup_seed function in codegen.ml lacks SLOAD just after PUSHing a location of array (a seed) and thus says
“if some array is not initialized, then overwrite Program Counter to 1.”
“if some array is initialized, then abort this work.”
This is a fatal bug.

And I warn NOT TO USE bamboo at all. (maybe you know well)
It’s fully useless because it’s designed lacking the ability of designing formality at all.
If tests are done correctly, this must be avoided, and all the source code looks like this.

I concluded bamboo is an insane compiler as its unreadability indicates.

Pen compiler is planned to have “Internal Type checker” .
This is a new type of type checking.

External Type Check is a statically type checking as done on a program run by a single computer before its code generation. Thus, the generated machine code does not have type checking process at all.
Internal Type Check is a type checking run dynamically but statically embedded in the compiled code, which means any computer in the world who runs the program must run the type checker. This is a decentralized Type Checker.

( @pirapira 's fatal mistake was the confusion between External Type Check and Internal Type Check. )

With Linear Type Checking or, Quantitative Type Theory (a practical Dependent Linear Type Theory introduced in 2016-2018) ,
we can determine how many times each function has to be used.
Pen compiler is planned to integrate Linear Type System with the Internal Type Checking first.

Now pen compiler has primitive lambda calculus and let-in syntax.
It’s the starting point of functional style language and modern static type checker.
Check, review, and criticize!