技育展2023に参加しました

技育展 2023 に参加しました．僕は個人開発した定理証明支援系を発表しました．ブロック予選と決勝大会（決勝大会はさらにファーストラウンドとファイナルラウンドに細分化される）があり，僕はファーストラウンド敗退という結果でした．

この記事では，まず初めに，この記事に添付する発表資料を補完する形で，定理証明支援系を作った動機や各開発アプローチの採用理由を述べています．最後に，技育展 2023 に参加した感想を雑多に書き殴っています．

技育展とは

技育展とは，サポーターズさんが主催する，学生のためのピッチコンテストです．発表する作品は自分達の手で作ったものならなんでもよく，様々な開発背景のある全作品が無差別級に鎬を削りあいます．詳細は技育展の公式 Web ページをご覧ください．

発表した作品

Calculus of inductive constructions (CIC) を理論的基盤とする，ブロックベースで証明を記述可能な日本語定理証明支援系「かたぱ」を発表しました．発表資料は以下:

作った動機

主に以下の 3 つです:

1. 何らかの新規性があるプログラミング言語を作りたかった
2. それなりに複雑な型システムを作りたかった
3. 定理証明支援系に触れて初めて証明の進め方が体に馴染んだ感覚があり，より多くの人にもこの体験を得てもらいたかったから

1 に関して，僕は元々プログラミング言語自体が好きで，これまで既存のプログラミング言語の処理系のミニ版を度々作ったりしていました．その中で，既存の言語の再実装ではなく，何らかの新規性がある言語を作りたいとも考えていました．そのとき，ある友人から「オブジェクト指向の日本語プログラミング言語を作ってみると面白そう」的なアドバイスをもらい，日本語プログラミング言語の文脈で着手されていなかった「日本語 × 定理証明支援系」というテーマを思いつきました．

2 に関して，ここは勉強目的が強い動機になります．かたぱの理論的基盤の CIC は世の中で広く使われている定理証明支援系 Coq の基盤ということもあって相当強力なので，これに基づく型システムが実装できるなら大抵の型システムは実装できるほどの力が付くだろう，みたいなお気持ちがありました．関連して，定理証明支援系の実装は，Coq の中で何が起こっているのか理解する一助になるとも考えていました．

3 に関して，これはかたぱのゴール「日本語ネイティブの数学初学者が効率よく証明の学習を進められる」に強く影響している動機になります．めちゃくちゃ雑に言うと定理証明支援系の布教目的です．真面目に説明すると，元々，僕は型といった形式手法に興味はあるものの，数学的な証明自体はすこぶる苦手でした．学校のテストの点数が著しく悪いことはなかったのですが，表明をなぞっているだけで自分の身になっていない感覚がありました．そんなある日，「Coq/SSReflect/MathComp による定理証明」という本や「プログラミング Coq」という記事に出会い，Coq を勉強していく中で，これまでふわふわしていた証明の進め方が体に馴染んできた感覚がありました．おそらく，証明のセルフチェックができるために自分一人でトライ&エラーを回しやすかったり，証明の行間が極端に小さかったり，証明の書き方が明確に決まっていたり¹，みたいなところが効いているのだと思っています．Coq のおかげで，今では証明に対する印象を「得意ではないけれど，ちょっと好きかも」くらいのレベルに押し上げられました．このような体験をあわよくば中学生のときに得られていると，今の僕はかなり違った生き方をしているんだろうなーと思うところがあったりします．一方で，中学生のときの僕は英語を読み書きできないので（今でもあまりできないですが……），Coq の勉強は相当パワーがないと難しいです．そこで，日本語で読み書きできる定理証明支援系が存在していると，当時の僕のような人に対する助けになるんじゃないかと考えました．

各アプローチの採用理由

「証明のセルフチェックの難しさ」に対するアプローチの採用理由は動機 2 によります．

「既存の定理証明支援系の学習コストの高さ」に対して，日本語の構文の採用理由は動機 3 によります．Scratch 風のブロックベースの UI/UX を採用している理由は，以下の 2 つになります:

1. 構文エラーを発生させないため
2. 実装コストを削減するため

1 は動機 3 に関連するものになります．2 に関しては，最初は「Polymorphic Blocks: Formalism-Inspired UI for Structured Connectors」のように，かたぱの名の通りマジでパズルを解くみたいな UI/UX にする案もあったのですが，この研究内容を CIC に拡張・実装していると技育展のエントリーが間に合わないと考え（僕の場合，およそ 2 ヶ月で動くものを作る必要がありました），Google が開発している Blockly を用いたブロックベースの UI/UX を採用しました．

「既存の定理証明支援系の人間可読性に関するジレンマ」に対するアプローチの採用理由は，ブロックベースの UI/UX を既に採用しているという前提のもとで，他に候補があった訳ではないので特にないです．証明の実行中に得られる情報を使ったら証明をもっと読みやすくできるよね，みたいなアイディアをもとに作ってみた感じです．

余談

かたぱの型システムの部分は当初 OCaml で作っていました．やっぱりメタランゲージでランゲージを作りたいじゃないですか……²．

開発を進める中でその気持ちを数々の辛みが上回ってきたので，現在は TypeScript で書き直されています．念のため補足しておくと，その辛みはかたぱのクライアントサイドが React × TypeScript 製なことに由来しており，OCaml 自体が辛いってことではないです．OCaml は良い言語だよ，全ホモ・サピエンス書きましょう．

なお，かたぱは将来的に OSS として公開予定なのですが，型システムの実装が完全に終わってからの公開になります．具体的には Inductive types という機能の実装が終わってません（超絶ムズイ）．型システムを自作する動機は勉強目的が大きいので，ここは個人でもくもくやりたいと考えています．

雑多な感想

特にまとまりのない感想です．次の写真は甲子園の土:

よかったこと

何より決勝大会がオフライン開催だったところがよかったです．僕はシャイなので人が多くてキョドりまくりでしたが，それでも会話が自然発生したり，可変な人数で話せたり，初めて名刺交換できたり，凄まじく楽しかったです．偶然隣にいた人に話しかけて，それがきっかけで仲良くなるみたいな体験はオンラインだとホント難しいです．オフライン開催のネックとして，移動にお金や時間がかかってしまったり，平日開催の場合は時間の都合をつけづらいなどがありますが，今回はサポーターズさんから交通費を支給していただけたり，土曜日の開催だったりと配慮もてんこ盛りでした．

オフライン開催の良さと関連して，楓さんや加藤さん，就活中にサポートしていただいた人事の方など，これまでお世話になった方々にご挨拶できたのも個人的によかったです．僕は 2022 年 5 月あたりにサポーターズさんを知ったのですが，このときの出会いがなかったら今の僕はないと本気で考えています．僕にとって，技育 CAMP ハッカソンや技育展という場の存在が大きな助けや救いになっていました．また，イベントを通して多種多様な人たちと関わることができ，技術面だけでなく人間的にも成長できたと思ってます．まずい，感情がクソデカくなってきた．本当に深く深く感謝です．

東大という雲の上の場所で発表できたこともよかったです．僕にも自分が所属する大学を公表するのにやや抵抗感を覚えるくらいの学歴コンプはあるので，東大で発表ができたのはそんな自分を肯定する自信になってくれるんじゃないかなと期待してます．まぁその会場を用意していただいたのはサポーターズさんなんですけど．本当に足を向けて寝られません．

よかったことかどうか謎ですが，ある人と Coq の話をしているとき，「大学の講義で Coq を学んだ」という情報からその人が所属する大学を特定できたことがおもろかったです³．

よくなかったこと

自分の発表がホントよくなかったです．他の方の発表が始まるまでは「スライドを手元で見てもらったらスライドの情報量多くても問題なしや！」みたいにゆるふわ考えてしまってたんですが，発表が始まってからすぐに考え直しました．他の方の発表は 3 分の中で理解できるよう綺麗にまとめられているんですよね．自分の発表の仕方は 3 分で発表を収められないことの単なる逃げだなとかなり反省していました．定理証明支援系という一般的ではない対象の発表ではありますが，もっと伝わる発表があったんじゃないかと思います．決勝までに開発面でやれることはやったつもりなので，発表がよくなかったのが本当に悔しいです．自宅に帰って母から慰めの言葉をもらったとき，自分が負けたことを強く実感してさらに悔しかったです．

個人開発なのでチームで打ち上げができなかったこともよくなかったです．技育展のあとは一人で観光名所の鳥貴族（高知には鳥貴族がない）に行ったりしてましたが，勇気を出して他の個人開発者を誘ったらよかったです．

名刺が大量に余ったのもよくなかったかも．200 枚はどう考えても刷り過ぎた．今度僕と会った人は 5 枚もらってください．

その他

当たり前っちゃ当たり前ですが，やっぱり積み上げの多さは強さに直結するなと思いました．プロトタイプを何十個も作っていたり，手元から離れた現場で既に動いていたり，ユーザ数や売上が凄まじかったり，強すぎました．技育展はハッカソンと違って作品にかけられる時間についても無差別級ですからね．かたぱも今後積み上げを重ねて，少しでもゴールに近づけるよう頑張りたいです．

まとめ

最高のイベントでした．結果はファーストラウンド敗退でしたが，プログラミング言語の探求をはじめ，自分の大きな糧になったと思います．24 卒なので今後サポーターズさんを利用する機会は減ってしまうのですが，サポーターズさんが今後もカッコイイオトナを増やしていくことを陰ながら応援したいです．ありがとうございました！！！！！