Formal Type System On EVM
The Flow of Compiler : Pen
****************************************************************************************
* *
* *
* pen source code *
* | *
* v *
* +----------+----------+ *
* | type checker | *
* +---------------------+ *
* | *
* v *
* Pen Intermediate Representation *
* | *
* v *
* +----------+----------+ *
* | Gas Checker | *
* +----------+----------+ *
* | *
* v *
* Gas Checked PIR(Assembly) *
* | *
* v *
* +----------+----------+ *
* | Code Generator | *
* +----------+----------+ *
* | *
* v *
* EVM Machine Code *
* *
* *
* *
* *
****************************************************************************************
# Todo Type Theory
Before starting, we should get very accustomed to Type Theories.
- Type Theory
- Implement Dependent Type Checker
# Research Todo
## Loops in Typed Blockchain Programming Languages
### What about adding fix to bamboo ?
bamboo by pirapira ( around 2018 version ) analysis : see https://github.com/ghasshee/pen
- Bamboo may not have `fix` operator which can be typed with Infinite Type
- Analyse Code Generator of bamboo
### Coq's Well Foundness
- Coq Style programming Language i.e. forbid increasing recursion
- Requisity of "Well Foundedness" : A set is "Well Founded" if it has a minimum element.
## Type Inference and Dependent Types
- Motivation : To what extent, Type Inference is Practical
* Let Polymorphism (mono types)
* System F (poly types)
* Rank 2 polymorphism
- Dependent Types v.s. Type Inference
##
# Gas Leak Checker
point out where Gas is used
A contract say
" If someone send money to this contract,
then they can withdraw what they sent. "
Borrow checker
This data has life time and when borrowing it, it is locked.
# Assembly
How to lock data
What is the specification of MIR ?
This Contract has a lifetime
if someone
# Error handling
## Formal Contract
Formal Contract cannot have any kind of errors since it has been proved that the code of the contract has no bugs.
## Not Formal Contract ?
if a deployed contract detect a run time error, i.e. it is a contract written by a Non Formal Laguage.
# How to one can know which contract on the blockchain is formal and which is not ?
Byte Code Specification
# Prerequisities
## The Fundamental Base of Type Theory
- Types and Programming Languages
- Advanced Topics in Types and Programming Languages
- Homotopy Type Theory Book (Appendix A)
- Local Type Inference [Pierce 98]
## Papers about blockchain programmings
# What to do
## List EVM Machine Codes
## primitives in Type Language
## Type Checking System
* if t then t else t
* λx. t
*