Type-based FV of smart contracts

Fomality

Used for Moon Browser project

Formally verified Dapp browser, download all codes of UI + smart contract

Fomality

New functional language implemended

Baed on Cedilleum

Cedilleum: はアイオワ大学の教授Aaron Stamp氏により開発され、Grant Wave2に採択

シンプルな型理論

Compiled to Abstract Calculus and then (eWASM)

独自の言語を作った理由

「Agda, Idris, Coqなどの定理証明支援系は高階関数にかなり依存しており、専用の実行環境やガベージコレクションを必要とし、実行を大変なものにしてしまう」から

Abstract Calculus

チューリングマシンとラムダ式を合わせた新しい計算モデルを利用

ラムダ式のような高階関数, map, fold

チューリングマシンのように it has a very clear cost model, being evaluated in a series of constant-time operations that translate well to hardware code, requires no closures, garbage collection and is is optimal

独自VMとしてFVMも提案

Abstract Calculusの並列性を活かすための

EVMやeWASMの代替

Rholang

RChainのスマートコントラクト言語

並行プログラミング

ρ-calculus

カリーハワードベースの定理証明を用いる模様

Plutus

Cardanoのスマートコントラクト言語

λ計算

F*を経由したSolidity, EVMバイトコードの形式的検証

SolidityをF*にtranslateしたり、EVMバイトコードをF*にdecompileし、F*の型推論を使って形式的検証

F*はMicrosoft Researchが開発した定理証明向き言語

Solidityのサブセット。ループなどは排除されている。

https://gyazo.com/a872839e537a75af692f4038fdd13199

Zen protocol

F*のサブセットでスマートコントラクトをかく

UTXO型

Idrisによるコントラクトの実装

Idrisは依存型ありの純粋関数型言語(coqやAgda, ATSもそう)

EVMを吐いてみたがめちゃめちゃ長くなったっぽい

Others

形式的検証をそこまで特徴にしているわけではない(?)が、セキュリティを重視した他の言語

Pyramid

Lisp方言のSchemeの方言

Grant Wave3採択

開発者による参考記事

Bamboo

コーネル大学が開発を進めると宣言している(が、まだ進んでなさそう？)

tail call

Obsidian

カーネギーメロン大学

typestate-oriented language

状態を第一級の型とするもの？

tail call

ユーザーテストをしながら言語をデザインするこだわり

内容は薄い

Future Workで将来的には形式的手法も取り入れていく

その他