暑い。
先日、福岡に行きました。ブロックチェーンじゃないです。子供が 野球見たいxラーメン食べたい と四六時中言っているので福岡まで行ってきたんです。結果ホークスは負けました。ラーメンは美味しいいうて食べてました。
博多の街で面白いものを見つけましたわ:
「おポンプ様」です。戦時中の火災消化や、戦後の渇水時にも使われたそうで、その道具が神格化されて街に鎮座されているのは興味深い。今でも頑張ってハンドルを動かすと水がでるそうです。実際でました。こういう二連のポンプは珍しいそうです。確かに東京の谷中に住んでいた時は地域にポンプが二つほどあったけど、単発だったな。
風説を流布して価格上昇したところを売り抜けて後はシラネ、ってのを pump and dump と言って、あんまりいい意味がないんですが、これは良い O’Pump sama でした。
ブロックチェーンのサマースクールやります
閑話休題。そんな暑い中ですが、八月末に以下の予定で「ブロックチェーンと形式検証」というお題目で一日サマースクールをします:
まず東京:
PPLサマースクール2019 「ブロックチェーンと形式検証」
日本ソフトウェア科学会 (JSSST) プログラミング論研究会 (PPL) 主催
日本ソフトウェア科学会第36回大会 併設企画講師：古瀬 淳（ダイラムダ株式会社）
2019年8月26日(月) 10時〜17時（予定）
芝浦工業大学芝浦キャンパス
(〒108-8548東京都港区芝浦3-9-14)
そして台北:
2019「邏輯、語言與計算」暑期研習營 (FLOLAC'19)
日期：2019 年 8 月 19 日 (週一) 至 8 月 30 日 (週五)，共計十天。
時間：每週一至週五早上九點至下午五點。
地點：台灣大學管理學院 (待定)。
PPLのサマースクールについては、弊社技術顧問をやっていただいている京都大学の末永先生がご提案、ご尽力により実現したものです。
台北の方は、台湾でTezos開発をしている Nine Chapters の人たちが東京でやるなら台北でもできる？って聞いてきたので引き受けました。英語で授業やったことないねんけど。これは10日もあるサマースクールで、毎年やっているようです。繁体字の説明から類推するに、なかなかハードですね。最終日には試験があるようです。このうちの一日頂いてお話をします。
内容
どちらもブロックチェーンについての知識は仮定せず、基礎から話すつもりですが、 対象はプログラミング理論を専攻している学士の方です。 ブロックチェーンというと投機とか詐欺とか窃盗とかGAFAこわいとか、私がサトシですとか、いや俺がサトシだとか、胡散臭い話ばかりですが、落ち着いて中身を見ると分散システムとプログラミング言語の話が多いので、理論寄りのコンピュータ・サイエンス研究として魅力のある分野だという事をお伝えするのを目標としています。
Tezosはブロックチェーン技術の中で特に形式検証に力を入れているプロトコルです。 サマースクールでは、実際のTezosでの形式検証技術の適用についてもできる限り紹介してみるつもりです。リサーチトピックなのでなかなか深いところまでできるか、難しいですが…
とりあえずスライドは一通り作りました。こんな感じ。 英語は日本語よりスペースを取るので、まず英語で書いてみました:
ハンズオンもします
こういう話は実際のシステムを触ってみないと実感がわかない部分もありますので、後の1/3でTezosブロックチェーンを実際に触る実習も行います。環境はおそらく一週間前くらいに公開するつもりですが、Docker を使います。Docker が外部ネットワークと通信できる事が必要です。
皆さんのご参加をお待ちしています。