東京と台北のサマースクールで授業をしました

8月の最後の週、東京と台北でサマースクールの授業を二本持たせていただきました:

PPLサマースクール2019 「ブロックチェーンと形式検証」
8/26、 於 芝浦工業大学芝浦キャンパス
FLOLAC'19 「邏輯、語言與計算」暑期研習營
8/29、於 台湾大学

PPLのサマースクールは一日だけ、単一のテーマのものです。 FLOLACは10日連続のサマースクールの講義最終日に一日いただきました。 どちらも全長6時間、4時間私が喋った後は2時間 Tezos を使った簡単な実習を行いました。 内容もどちらも同じ。言語が日本語と英語くらいの違いしかありません。

PPLは70人弱、FLOLACは約40人くらいの参加者をいただきました。

スライドはこちら:

Blockchain and formal verification (Japanese) from Jun Furuse
Blockchain and Formal verificatio (English) from Jun Furuse

今年の頭からいろんなところでブロックチェーン関連の話をさせていただいてきて、 スライドも話も毎回修正を繰り返してきましたが、このサマースクールで一定の点まで完成した感があります。 量は170頁超えです。まあ一枚2分とすれば6時間だとちょうどそのくらいですね。 何度もこういう話をしてきて思うんですが、私は長い時間に対してはわりとあまり考えずに きっちり時間に合わせて話ができる能力があるみたいです。

実は英語で授業をやるのは初めてだったので、台湾ではかなり緊張しましたが、 後半になると慣れてきて、まあ適当な英語だけど話せるものですね。 あと偶然ですが今月末は弊社の期末でもありましたので、出張しながら書類もこなすのが大変でした。

さてサマースクールの内容ですが、

  • 通貨の進化の歴史
  • ブロックチェーンの概要
  • PoWとPoSの原理
  • Tezosの特徴の紹介
  • 形式検証の概要とTezosで行われている事例の紹介
  • Tezosを使ったハンズオン

です。二回とも対象はコンピュータサイエンスを専攻している大学院生以上を対象としています。 ブロックチェーンの原理を知らないと仮定しているので、そのあたりの導入は丁寧にやろうとしています。 結果、形式検証手法は紹介だけしかできなくなってしまいました。授業で4時間ではちょっと 完全に新しいバックグラウンドを紹介して、その問題領域を詳しく解説する、というのは時間が 足りないのかなあ、という気がします。物足りなかった方も多かったと思うので、 次の機会があれば、ブロックチェーン部分の知識は仮定して、より深い検証の話ができるようにしたいと思います。ただそのためには各研究事例についての深い理解が私自身に必要なので、大変ですね。精進したいと思います。

今回の実習ではスマートコントラクトの高級言語にLIGOを使いました。 この言語はまだ本当に開発中で実用には使えないというのが正直なところです。わりと頑張って サマースクールの直前まで足りない機能を足したり、バグを直したりしました。これが今回一番大変でした。頑張ったおかげでMLが書ける人なら、それでも所々引っかかりつつもスマートコントラクトを書けたと思います。この点ではPPLのサマースクールは参加者に経験者がたくさんいらっしゃったので、MLの説明をほぼ飛ばして話を進めることができました。FLOLACではちょっと厳しい感じがありました。ブロックチェーンの基礎原理と形式検証の事例を話した後に、関数型プログラミングを教えた上でスマートコントラクトハンズオンをやるのは6時間では到底足りません。

さて、台北ですが、私は訪れるのが今回が初めてでした。ほとんどずっとホテルに籠って授業の準備や弊社の期末処理をしていたのですが、少しは街を歩くことができました。とても楽しかった。もっと早く行ったら良かったです。

ホテルは台湾大学のそばにあったので、台湾大学のキャンパスをウロウロしましたが、旧帝大の名残を感じさせる校舎がたくさんあり、とても好きになりました。私が学生だった頃の京都大学にもわりと古くてボロい校舎が残っていたものですが、25年後に戻ってみると、大半は新しいピカピカの、でもつまらないビルに変わってしまっていて、まあ耐震性とかで必要だと思うし、毎日使っている人には新しい方が便利だとは承知しているんですが、あの学問の垢が積もった重い雰囲気がだいぶ失われてしまったなあと思っていたんです。台湾大学にはそれがすごく残っていていいなあと思いました。緑もすごく多い。

キャンパス内にはいくつか無料の小博物館があり、植物標本室を見学しました。繁体字が美しい。見ていると、台北帝大時代の資料も置いてありました。一応この辺りの歴史を知っている者としては色々な感情が生まれました。

大学近くにも夜市があり、以前住んでいたシンガポールでは禁止されホーカーセンターに集積された屋台が路上に並んでいるのを見ました。結局ショップハウス形態の屋台じゃない店で何度か食べましたが注文の仕方はシンガポールと同じだったので英語日本語が通じなくても全く問題なし。安いし美味しい。

いやーまた行きたいです。台湾にはNine Chaptersという会社があって、こちらもTezosの開発を行っています。共同で仕事をやっていくつもりなので、またすぐいけますね!!