OCamlとCoqでブロックチェーンプログラミング

OCamlとCoqでブロックチェーンプログラミング

yoshihiro503氏（以下、yoshihiro503）：みなさんこんにちは。こういう鶏のアイコンのyoshihiro503です。今日「OCamlは良いぞ！」という話をします。株式会社ドワンゴのDMC開発部に所属しています。

簡単に自己紹介をします。私はOCamlの作者であるガリグ研究室の出身です。昔、OCamlミーティングや関数プログラミングの集いを主催していました。昔は名古屋に住んでいました。Proof Summitというイベントを毎年やっていて、実は2011年からやっています。Proof Summitは今年もやりますので、証明とか形式検証とか関数プログラミングが好きな人は、おもしろいのでぜひ来てください。無料です。発表者も募集中です。

TaPL（Types and Programming Languages）という、おもしろい本があるんですけど、それの翻訳をやっていて、名古屋大学で客員准教授をやっていたりします。

Types and Programming Languages (The MIT Press) (English Edition)

ブロックチェーンとTezos

「ブロックチェーンとは」。暗号通貨とかを聞いたことあるかもしれないんですけど、ブロックチェーンにあまり詳しくない方もここにはいると思います。取引をブロックに詰め込んでチェーンにつなぐ、すごいやつなんですけど、これは通貨みたいなお金をやり取りするものに使われていて、すごいですよね？　すごいです。

（会場笑）

ブロックチェーンの1つの大きな特徴としてスマートコントラクトがあります。スマートコントラクトというのは、お金の取引の中にプログラムを埋め込むみたいなことなんですね。その通貨ごとに独自プログラミング言語があって、そのプログラムを埋め込んでいく。プログラマはそのサードパーティー製のアプリケーションを、そのブロックチェーンの上で動かせるんですよ。

すごくないですか!?　これはプログラマだったらドキドキワクワクする話で、僕もあまり暗号通貨とかよくわからない状態だったんですけど、プログラムを通貨の中に埋め込んで、それがみんなの生活の役に立つことがすごいおもしろいなと。「しかも言語処理じゃん！」みたいな感じですごい心躍る感じです。

ここで1つ、おもしろい通貨を紹介します。「Tezos」というブロックチェーンプロトコルです。これはOCamlで全部書かれているすごいやつなんですよ。OCamlで書かれています。それでTezosという通貨もあるんですね。あまり有名じゃなくてみんな知らないし、普通によくあるところで取引されていないんですけど、そういうものがあるんですよ。それでOCamlで書かれている。

今、パリにいるOCamlerたちがわりと中心となって開発しています。コアの部分は全部OCamlで書かれています。関数型プログラミングと、あとは形式検証ですね。証明を使ってすごい安全なブロックチェーンのプロトコルを実現しようとやっています。これはすごいですね。

さらに日本では、日本にも拠点がありまして京都にキャメロバ様……昔キャメロバ様だったんですけど、今よく見たらキャメロバ様じゃなくなってたので……。

（会場笑）

CamlSpotter、OCaml界隈ではスーパー有名な日本人の人がいるんですけど、その人が中心になって開発しています。さらにガリグ先生とか京大の五十嵐先生たち……これはJavaにジェネリックスを入れたりしているのも有名ですね。主に研究の分類でコミットして、熱い関数型で熱い通貨になっています。

スマートコントラクトについて

さらに「そのスマートコントラクトはどうなっているんだ!?」と言ったら、スマートコントラクトも言語もfunctionalなんですね。すごいですよね。それで、スマートコントラクトに関して通貨ごとに何か言語があると言いましたけど、Tezosの場合はMichelsonという名前の言語があります。

これは、静的型付きなんです。スマートコントラクトの言語はローレベルな言語でスタック言語なんですけど、スタックに型が付いているんですね。しかも処理系の実装が純粋関数的に提供されていて、さらにCoqでの証明が付いています。すごいやつです。こんな通貨は他にないですよ。

（スライドを指して）Michelsonのコード例はこんな感じですごくローレベルです。これはリストが与えられたときに、リストのリバースをする処理で、LOOPというものが真ん中あたりにあるんですけど、そのLOOPをしながらリストをクルクル回してリバースしていくんですけど、読めないですよね。

Michelsonは、かなりローレベルのコードなので、このレベルだったらギリギリ読めても大きくなるとだんだん人間には不可能になっています。

LIGOとは何か

そんなあなたのために高級言語があります。この「LIGO」です。いろいろあるんですけど、まだ開発中なので迷う人がいるかもしれないですけど、私は今後このLIGOを押していくのではないかとみています。

それで、このLIGOというやつがさっきの言語のよりリッチなやつで、このLIGOで人間が書くとコンパイルして、さっきのMichelsonに変換してくれる感じです。LIGOというのは複数のシンタックスをサポートしていて、PascaLIGOとCameLIGOという2つなんですけど、3つ目のReasonLIGOはComing Soonとなっているので、近日そういうのが入るかもしれないです。

1個目はPascal風のコードです。2個目はOCaml風です。この真ん中のOCaml風の言語を使ってスマートコントラクトを関数型プログラムのままみんな書けるのがすごいおもしろいと思います。これのクエリがfunctionalなんですよね。すごく安全に、金融のアプリケーションを書くのに適しています。

他の通貨がどんな言語でやっているかと言ったら、一番有名なイーサリアムはSolidityというJavaScript風の命令型言語でやっているんですね。「それで本当にあなたの金融資産を守れるのか？」と不安になる……。ここはちょっとカットしたほうがいいかも。

（会場笑）

でも、その辺を固くやろうという強い信念が設計にあらわれていますよね。CameLIGOのコード例を見ると、こんな感じでバリアント型を書けるんですね。これはOCamlで見たことがある人から見るとまんまOCamlですよね。パターンマッチも使えてすごいわかりやすい。これで動くんですね。

まとめます。functionalな暗号通貨Tezosをみなさんにご紹介しました。contract言語もfunctional。形式的検証というのをやっていくぞ！　というすごい意思の溢れるおもしろい言語だと思いました。

宣伝します。「PPLサマースクール」という日本ソフトウェア学会が主催している学術的なイベントの併設イベントがあるんですけど、そこでさっきのキャメロバ様ですね。本名が古瀬さんというんですけど、その人が講師になってブロックチェーンを「みんなで手を動かすブロックチェーンをやろうぜ！」というイベントをやります。これはOCamlや関数型のシステムがどう証明されていくかなど、そういった説明もあるのでおすすめです。

これは毎年あるんですけど今年は芝浦工業大学という学校でやるみたいなので、みなさんもこれに参加したらおもしろいと思います。

あともう1つ宣伝。Proof Summitというのを毎年やるって言ってましたけど今年もやります。9月28日で、参加は無料です。発表者がまだ1人もいないのに昨日公開したら50人上回っちゃいました。

（会場笑）

誰が発表するか誰にもわからないのにみんな待ってたかのように、1日で50人上回るというなんかおもしろいということがあって、発表者募集中です。証明とかそういうのを「やってみた！」とか「やってみよう！」と思っている方はぜひ何かネタを提供してくださると助かります。

以上です。ありがとうございました。

（会場拍手）

Tezosはどれくらい使われているか？

司会者：少し時間がございますので、よろしければ質疑応答をして……。

@yoshihiro503：はい、じゃあ質問をください。5分ぐらい質問ができるという感じですかね。

質問者1：Tezosというのは今どれぐらい使われている感じですか？

@yoshihiro503：「Tezosがどれくらい使われているか」ということですね。すみません。私はちょっとそういう実用的なことはあまり詳しくないです。

（会場笑）

ないですけど、聞いた話によれば不動産の取引を国際的にみんなでちょっとずつ出資して「インドネシアの大きな観光リゾートを買うぞ！」みたいなことをやるとか、巨額な・長期的な・国際的な投資に使われている話を聞いたことあります。

質問者1：ありがとうございます。

質問者2：Tezosで形式証明をどんどんやっていくというお話だったと思うんですけど、今目標とするゴールまでどれくらい証明が進んでいるんですか？

@yoshihiro503：なるほど。「どれくらい証明ができているか」という話ですね。1つは何を証明するかというところで、私が考えているのは2つの大きな課題があると思っています。

1つはさっき言ったスマートコントラクトのプログラミング言語みたいなものがあるので、その言語設計の安全性を証明すること。もう1つは、Tezosのブロックチェーンのコンセンサスプロトコルがあると思うんですけど、そもそもTezosのコードベースですね。これが正しいかどうかの検証。

この2つが必要だと思っていて、私も全部のソースコードを眺めたわけではないのですが、今のところはっきりあるのはスマートコントラクトの言語の処理というのが形式的に、つまりさっきのMichelsonですね。ローレベルなMichelsonに関しては形式的な検証で、それは1つ大きいですね。クエリのファンクションでいろいろなものが作られているのでその辺が他の言語に比べると、かなりリーチが近いのかなと思っています。

質問者2：ありがとうございました。

質問者3：内容に関してではないんですけど、どうして「LIGO」という名前にしたんですか？　というのがすごく気になってライゴという重力波の望遠鏡があって名前が商標が取れないじゃないかなと気になりました（笑）。

@yoshihiro503：あー……。

（会場笑）

ちょっと命名に関してはちょっと私は知らない……。ググったら何かわかるかもしれない。

質問者3：はい。ありがとうございます。

@yoshihiro503：じゃあ終わりです。じゃあ、みなさんありがとうございました。

（会場拍手）