採択
2026/01/10 16:20〜
特別会議室
スポンサー LT
スポンサー

推し活の延長線でDevRelが立ち上がった1年間

TechTrainでCSとして働く中で、エンジニアとのやり取りやGitHubの読み込みを通じて、その魅力を言語化してきました。
多方面でエンジニアの推し活を続けるうちに、いつの間にかDevRelと呼ばれる役割を担うようになっていました。

本トークでは、技術者出身ではない立場から見えてきたDevRelの仕事と、その面白さを紹介します。
本トークを通して、私が関わっているTechTrainにも、少しでも興味を持っていただけたら嬉しいです。

採択
2026/01/10 16:40〜
特別会議室
スポンサー LT
スポンサー

サイボウズには100名以上の社員が出演する"夏フェス"があるって本当?

oguemon_com おぐえもん

寒い冬なので暑い夏の話をします!
サイボウズでは、夏に多くの社員が集まりブログ記事を怒涛のように投稿する夏フェス「CYBOZU SUMMER BLOG FES」を2024年から毎年開催しています。
今年はおよそ120記事が投稿され、投稿した社員数も今年は100人を超えました。
ここでは、サイボウズの発信文化を象徴するこの祭の概要と、その運営の裏側を簡単に紹介します。
アドベントカレンダーもいいけど、記事が埋もれにくい夏の季節に「フェス」をやる選択肢を皆さんにお届け!

採択
2026/01/10 16:30〜
Room 205/206
スポンサー LT
スポンサー

フロントエンド開発の勘所 - 複数事業を経験して見えた判断軸の違い -

久保 陽一郎

本 LT では、toB と toC で求められるフロントエンドエンジニアリングの勘所の違いについて、実際の事業開発の現場で得た経験をもとに整理し、再現性のある学びとして共有します。
フロントエンドエンジニアは、UI 実装や技術選定だけでなくプロダクトの価値をユーザーに届けるための「最後の砦」としての役割を担います。しかし、その「価値」の定義は toB と toC で大きく異なります。toC では「多くのユーザーにどう魅力的に届けるか」が重視される一方で、toB では「限られたユーザーが日々の業務をいかに速く・正確にこなせるか」が価値の中心になります。
発表者はサイバーエージェントに新卒で入社し、フロントエンドエンジニアとして約 10 年間異なる性質を持つ複数の事業部で開発に携わってきました。
サイバーエージェントには大きく分けて以下の 3 つの事業領域があり、発表者はそのすべてに所属・関与した経験があります。

・ゲーム事業部
主に toC 向けのスマートフォンゲームを中心とした事業領域です。
フロントエンドとしては、ゲームのプロモーション用 LP の制作や、ゲーム内のお知らせ・イベント告知画面などを Web ページとして実装するケースが多くあります。特にゲーム内お知らせ画面などは緊急対応としてプランナー等非エンジニアが直接編集するケースなどもあります。
この領域では、短期間での大量リリースやキャンペーン単位での開発、タイトルごとのビジュアル的な細かいチューニングが求められるため、「スピード」「表現力」「運用のしやすさ」が重要になります。
多少の技術的負債よりも、ユーザー体験やタイミングを優先する判断が正解になる場面も多く、toC フロントエンド特有の意思決定が求められます。

・メディア事業部
ブログ、ニュース、動画配信サービスなど、Web を中心にプロダクトを展開する事業領域です。
SEO、パフォーマンス、アクセシビリティ、長期運用を前提とした設計などが重要になり、「作って終わり」ではなく「育て続けるフロントエンド」が求められます。
ユーザー数が非常に多いため、小さな実装ミスや設計判断がパフォーマンス低下や UX の悪化として顕在化しやすく、安定性と継続的改善のバランス感覚が重要になります。
その他にも動画配信の知識なども必要になるケースがあり、フロントエンドエンジニアとしては最も深い専門性を求められるかもしれません。

・広告事業部
インターネット広告配信を主軸としつつ、広告主や代理店向けの toB プロダクト(管理画面、分析ツール、運用支援ツールなど)を数多く手がけている事業領域です。
この領域のフロントエンドでは、見た目の派手さよりも堅牢性・拡張性・保守性・ドメイン理解に加え、使いやすさや作業工数の簡略化が強く求められます。
利用者は日常業務として長時間ツールを使い続けるため、UI のわずかな使いづらさや操作ステップの多さが直接的に業務コストの増加につながります。そのため、「正しく動く」だけでなく、「迷わず使える」「無駄な操作を減らす」ことがフロントエンドの重要な価値になります。

本 LT では、こうした前提をもとに、
・toB / toC でフロントエンドに期待される役割の違い
・技術選定や設計における「優先順位の変え方」
・UI / UX を考える際の視点の切り替え方
・事業が変わっても応用できるフロントエンドエンジニアの思考法
といった点を整理してお話しします。

特定のフレームワークやライブラリの解説に留まらず、「なぜその判断が必要だったのか」「別の事業だったらどう判断が変わるのか」という背景や考え方を共有することで、参加者が自身の現場に持ち帰って応用できる学びを提供することを目的としています。
toC プロダクトに携わっている方が toB 開発に関わる際の心構えとして、また toB プロダクトに携わる方が toC 的なスピード感や割り切りを理解するためのヒントとして、本 LT が役立つことを目指します。

採択
2026/01/10 15:00〜
Room 204
レギュラー

コンパイルエラーを元気に説明するLLMをファインチューンでつくる

kis きしだ なおき
kis

コンパイルエラー、あまり読みたくないですね。説明してほしい。そして、できれば元気に説明してほしい。
もちろん、最近のAIを使えば解説してくれます。
でも、そういったAIには課金か大きいモデルを動かせるハードウェアが必要です。毎日何万回も出すコンパイルエラーをそのたびに課金していたら破産してしまいますね。大きいモデルを動かす環境を用意するのも大変です。
そこで、小さいサイズのLLMをファインチューンして、コンパイルエラー説明専用のLLMを作れば、手元のパソコンでいくらでもコンパイルエラーを説明してくれるはずです。
ファインチューンにはデータセットが必要です。しかし元気にコンパイルエラーを説明するデータセットなんかありません。
このセッションでは、そんなファインチューンのためのデータセットの作成やファインチューンの方法を解説します。

採択
2026/01/10 12:20〜
Room 203
スポンサー講演
スポンサー

.NET 4.6 アプリのモダナイゼーションの挑戦 Part2:4.8.1に上げる?別ルート?"また来年"を禁止して、2026で終わらせます

ryosei_asai アサイクル株式会社 浅井了星

昨年(2025)は、.NET 4.6.2 を .NET 4.8.1 に移行して延命するのか、あるいは別の道(段階移行やモダナイズ)を取るのか―「どこへ向かうべきか。課題は何か。」をディスカッションしました。

Part2の今回は、その続きです。方針は2025年中に決める。2026年はステップを踏んで、1年で移行を完了する。それを本気でやり切るための話をします。

レガシー環境の困りごとは分かっているのに、移行が進まない理由はだいたい似ています。
「止められない」「怖い」「どこから触ればいいか分からない」―そして気づくと、また来年。

そこで本セッションでは、2025の分岐(4.8.1に上げる/別ルート)で整理した論点を踏まえつつ、2026にやることを “迷わない順番” に並べます。
移行を“壮大な理想”ではなく、1年で完走できるプロジェクトとして成立させるために、スコープの切り方、段階移行の組み方、品質の担保、切替の現実解まで、スポンサーセッションらしくテンポよく共有します。

採択
2026/01/10 16:20〜
Room 205/206
スポンサー LT
スポンサー

当社製品「memet」で選んだサービスに関するお話

io-murai

個人開発では、利用するサービスは責任も軽い分、気軽に選べますが会社組織として採用するサービスは関係者も多いことから 気軽に選ぶことは大変です。(メジャーで、有名なサービスだとしても です。)

当社が2025年の4月にサービスインしたテレビ電話サービス「memet」において採用したサービスの選定を例に、ソフトウェア開発者視点で どんなこと・ものを用意すれば ほかの会社に目が留まるようなサービスの提供ができそうか?ということをお話します。

採択
2026/01/10 16:40〜
Room 205/206
スポンサー LT
スポンサー

位置情報チャットアプリ spotch の開発をふりかえる

nemui_ft Misaki

今年度新たにリリースした位置情報チャットアプリ spotch(すぽっち)の開発のこれまでとこれからについて話します!

採択
2026/01/10 16:50〜
Room 205/206
スポンサー LT
スポンサー

迷わない!AI×MCP連携のリファレンスアーキテクチャ完全ガイド

sugimomoto 杉本 和也@CData Software Japan

CData Softwareでは、SalesforceやSAP、kintoneなど各種SaaSのビジネスデータと連携可能なMCP Server・マネージドMCPプラットフォームを提供しています。
しかし、MCPを活用してAIをビジネスに取り入れようとしても、利用するAIプラットフォーム(Claude、Amazon Bedrock、Microsoft Foundry)やエージェントサービス、LLM、ノーコードツールによって、最適なアーキテクチャは異なります。「結局、自分たちの環境ではどう実装すればいいの?」という疑問をお持ちの方も多いのではないでしょうか。
本セッションでは、各AIプラットフォームごとのMCP活用パターンを整理し、すぐに実践で参考にしていただけるリファレンスアーキテクチャをまとめてご紹介します。

採択
2026/01/09 12:20〜
Room 203
スポンサー講演
スポンサー

AIで急増した生産「量」の荒波を
CodeRabbitで乗りこなそう

goofmint CodeRabbit 中津川篤司

AI駆動開発によりコード生成量は飛躍的に増えましたが、その結果としてレビューや品質担保が人のボトルネックになりつつあります。本セッションでは、生産性ではなく生産量に着目し、AIコーディングエージェントが生み出す大量のコードをいかに制御し、信頼性・保守性を維持するかを整理します。
AIは増幅機であり、使い方次第で組織の課題も拡大します。レビューを前提とした開発フローの再設計と、AIコードレビューをガードレールとして活用する実践的なアプローチを紹介します。

採択
2026/01/09 12:20〜
Room 202
スポンサー講演
スポンサー

さくらインターネットの今

kameoncloud 亀田治伸、法林浩之

2025年はさくらインターネットにとって大きな変革の年でした。そんなさくらインターネットの近況を2名のエバンジェリストがお伝えします。

・亀田リージョン:さくらのクラウドの今 ~ハイパースケーラと肩を並べることはできたのか?~
・法林リージョン:さくらのAIとかGPUとかイベントとか 〜2026年もバク進します!〜

採択
2026/01/09 11:00〜
Room 201
基調講演
基調講演

2026年のソフトウェアエンジニアリング

t_wada 和田卓人

2025年はプログラミングの姿がすっかり変わったことで記憶に残る年になりました。 2026年、AIを活用したソフトウェア開発はより大規模化していきます。プログラミングを超えて、ソフトウェアエンジニアリングが必要な領域です。しかし、これまでのソフトウェアエンジニアリングは「人間が設計し、実装する」ことを暗黙の前提としていました。その前提が変わるとソフトウェアエンジニアリングはどう変わるのでしょうか。このセッションでは、AIとの協業が前提の2026年のソフトウェアエンジニアリングを考えていきます。

3
採択
2026/01/10 11:00〜
Room 203
基調講演
基調講演

旬のブリと旬の技術で楽しむ AI エージェント設計開発レシピ

chack411 井上 章

BuriKaigi ならではの「技術の旬」を楽しく理解できるセッションです。前菜は、業務を分解して繋ぐためのマルチエージェントオーケストレーションパターン。メインディッシュには、最新の Microsoft Agent Framework と Azure AI Foundry を中心に、 .NET 10 と Visual Studio 2026 / VS Code の新機能を添えます。デモを通じて、旬の技術を味わいながら AI エージェント設計開発の本質を楽しみましょう!

レギュラー

In January 2026, just "rails new".

PharaohKJ ふぁらお加藤

2026年1月9日か10日、その場で rails new してそのバージョンでライブコーディングします。
何を作るかはその場にいるみんなとノリで決めよう。

3
採択
2026/01/10 14:20〜
Room 204
レギュラー

Webサイトで縦書きを使う、縦書きのWebサイトを作る

berlysia berlysia

Webの縦書きについてご紹介します。

Webで縦書きをすることの意義について私が考えていること、
縦書きと横書きでは様々なことが異なっていて、ただ向きを変えるだけではないこと、
Webで縦書きを実現する現行の技術にはどのようなものがあるか、
縦書きを中心にしたWebサイトを構築しようとするとぶつかる困難と現状、
縦書きを取り巻く周辺状況、
をご紹介します。

Webの世界で縦書きができることと、それはとても日本語を扱う者にとってうれしいことであること、
そしてそれは日本語だけでなく、Webの世界にとっても、よいことなのだ、という主張をします。

Webフロントエンド領域に習熟する必要はなく、少しCSSの専門的な話をすることはありますが、すべて理解に十分な解説を付けます。

9
Lightning Talk

データが嘘をつく?時系列データ分析で暴いた、ダイエット失敗の真因と復活劇

doskoi64 どすこい

テーマ
体重、カロリー、歩数、アクティビティなどのヘルスケア由来の時系列データを分析し、データの不整合から真の問題を特定。記録の徹底と習慣化によって○○kg減量に成功した実践例を、技術的な分析手法とともに紹介します。

想定する参加者層
初心者〜中級者、データ分析に興味がある方、特別な前提知識は不要。ダイエットを始めようとしている方、健康診断の結果が気になる方

トーク概要
数年間で○○kg増えた体重。あすけんで記録したカロリーデータと、Apple Watchが記録した歩数・アクティビティデータは揃っていた。しかし分析してみると、記録されたカロリーでは体重が増えるはずがないという矛盾が浮かび上がった。
詳しく分析すると、いくつかの発見があった:

記録している期間は体重が減っている:カロリー記録がある期間をプロットすると右肩下がり
記録していない期間に体重が増えている:記録の空白期間と体重増加が相関
運動量の変化は体重にほとんど影響していない:歩数・アクティブカロリーと体重変化の相関が低い

この不整合から見えてきたのは、「記録していない日に高カロリーを摂取している」可能性。現在の体重が妥当だとすれば、問題は記録の抜け漏れにあることがわかった。
そこで徹底的に記録をつけるようにした結果、○○kg減量に成功。今度は食事記録とアクティビティデータが整合し、もっともらしい結果が得られた。人間行動心理学的にも、記録をつけることが習慣化を促すことは知られている。
このトークでは:

ヘルスケアデータの取得・可視化手法(Apple Watch、あすけんなどの連携)
時系列データ分析による不整合の発見プロセス
データから見えた「記録している時だけ痩せる」という真実
記録の徹底による習慣化と減量成功の実践例
エンジニアならではの「データドリブン」なダイエット戦略

を紹介します。
技術者として「測定できないものは改善できない」を体現し、データの嘘を見抜き、行動を変えた実体験です。結局、ダイエットは記録をサボらない自分との戦いでした。でも、そこにエンジニアリングで立ち向かいました。 健康が気になる方、データ分析を実生活に活かしたい方、ぜひご参加ください!

6
Lightning Talk

GASでスプレッドシートを操作するの面倒なのでORMっぽく操作できるライブラリ作ってみた

akahoshi_1421 あかほし

テーマ Google Apps Script, TypeScript, JavaScript
想定する参加者層 初学者から幅広く

内容
スプレッドシートをDBのように扱いたい時ありませんか?さらにこのDBから必要に応じて適当な情報を抜いたり差し込んだりしないといけない場合、GASを書いて自動化したくなるでしょう。
しかし、GASでスプレッドシートを操作するのは非常に面倒です。なぜならGASでデータを取得したい場合「このセル(あるいは行か列)からこのセルまでを数字で書かないといけない」ためです。増減するDBデータの中で対象データの行番号列番号位置を探し、データを抜いたり差し込んだりする手間のかかるコードを書かないといけません。
そこで私はORMのようにスプレッドシートを操作でき尚且つ、GASをローカルで開発できるツールを併用しJavaScriptだけではなくTypeScriptで開発できるライブラリを作ってみました!

2
はじめて枠🔰

AIエージェントに『人間らしさ』を教える苦闘記 〜エンジニア採用スカウトで妥協しない品質追求の試行錯誤〜

yokishava yokishava

エンジニア採用のスカウトメッセージで「ちゃんとレジュメを読んでくれた」と感じてもらえる文章をAIに生成させようとしたら、想像以上に大変でした。プロンプトエンジニアリング、RAG、ファインチューニング...次々と手法を試しても期待する品質に届かない。本セッションでは、AIの専門家ではないエンジニアが、特定ユースケースで「妥協しない品質」を実現するまでの泥臭い試行錯誤と、そこから得た知見を共有します。

これまでエンジニア採用で何百、何千のスカウト文章を書いてきて思いました。エンジニア採用の成功率を上げるには、候補者一人ひとりに向き合った「人間味のある」スカウトが大切です。でも、これをAIで自動化しようとしたら...予想以上の苦労が待っていました。

本セッションで話すこと:

  1. プロンプトエンジニアリングの限界

    • プロンプト改善で見えた「できること」と「できないこと」
    • 具体例:なぜAIは「〇〇の経験を活かして」という抽象的な表現に逃げるのか
  2. RAGで過去資産を活用...したかった

    • 過去のよくできたスカウト文章をRAGで学習させた結果
    • 文脈理解の落とし穴:なぜ的外れな引用をしてしまうのか
  3. 品質を妥協しないための工夫

    • 評価基準の明確化:「人間らしさ」を数値化する試み
    • ハイブリッドアプローチ:AIと人間の協調による品質担保

得られる知見:

  • MLエンジニアでなくても、AIの出力品質を改善できる実践的手法
  • 「期待する品質」を定義し、測定し、改善するフレームワーク
  • プロダクト開発でAIを活用する際の現実的な落としどころ

想定聴衆

  • AIを活用したプロダクト開発に興味があるエンジニア(初〜中級者向け)
  • 生成AIの実用化で苦労している方
  • 「AIに任せきり」ではなく品質にこだわりたいエンジニア
1
採択
2026/01/10 16:00〜
Room 204
Lightning Talk

MDN Web Docs に日本語翻訳でコントリビュート

uutan1108 うーたん

テーマ

Webに関する様々な情報がまとめられている MDN Web Docs に、日本語翻訳で貢献する方法を紹介します。OSSコントリビューションの第一歩として、翻訳を通じてWebの知識を広める活動を取り上げます。

想定する参加者層(前提知識)

GitやGitHubの基本操作(git pull / commit / push)を理解しており、Node.jsの環境が整っている初級〜中級レベルのWebエンジニアを想定しています。
OSSへの貢献に興味がある方、英語のドキュメント翻訳に挑戦してみたい方も歓迎です。

トーク概要

Webアプリケーション開発者であれば、一度は見たことがある MDN Web Docs。
この膨大なドキュメントの多くは、世界中の開発者コミュニティによって日々翻訳・更新されています。

本セッションでは、MDN Web Docs 日本語翻訳コミュニティのガイドラインに沿って、誰でも簡単に翻訳に参加できるプロセスを、初心者の立場からわかりやすく紹介します。
環境構築から翻訳の反映までの流れ、貢献時のポイント、そして実際に翻訳して感じた「MDN翻訳の面白さ」や「学び」を共有します。

英語が得意でなくても、翻訳活動は技術理解を深め、世界中のエンジニアとつながるきっかけになります。
OSSに関わる最初の一歩として、MDN翻訳の世界を一緒に覗いてみましょう!

10
採択
2026/01/09 15:40〜
Room 203
レギュラー

AIで開発はどれくらい加速したのか?AIエージェントによるコード生成を、現場の評価と研究開発の評価の両面からdeep diveしてみる

doskoi64 どすこい

テーマ

AIエージェントの導入によって、開発の現場は実際にどのくらい生産性が向上したかをテーマに、導入した現場での定量的な実測値とAIエージェントのベンチマークを深掘って考察した結果を発表します。
いくつかのAIエージェントの導入(2023年のCopilot、2024年のCursor、2025年のClaude Code)による社内でのマージ頻度やリードタイムの変化と考察、AIエージェントの研究開発の分野で参照されるHumanEval / SWE-Bench等のベンチマークの深掘り、そのベンチマークによる定量評価がどれくらい現場での定性的な評価と合っているのかを考察した内容を発表します。

想定する参加者層(前提知識)

機械学習やLLMに関する研究の知識などを必要とせず、コード生成をするAIエージェントを見聞きしただけの人にもわかりやすいような基礎からの発表にします。特に、ベンチマークについては、具体的にどのような課題があってどのように判定されているのかを噛み砕いて説明します。

トーク概要

本セッションでは、AI コードエージェント導入による開発加速の実態を、現場データとベンチマークの両面から整理してご報告します。
当社では 2023 年以降、その時点で有効と判断したコード生成 AI エージェントを導入してきました。マージ頻度やリードタイムの集計の結果、ある事業部では Cursor 導入後にマージ頻度がおよそ 3 倍、Claude Code 併用後にリードタイムがおよそ 1/2 となる変化を観測しました。この事実をもとに、「AI でどれくらい加速したのか」「どう評価すべきか」を定義し直します。

AI 導入初期はコード生成の品質が安定せず、人手による修正が前提となる場面が多いと感じていました。その後、モデル世代の変化に伴いコード生成の「精度」が向上し、コードエージェントの導入により開発体験が実際に変化した手応えがありました。ただし、この「精度」が具体的に何を指すのかに疑問を持ちました。変化量を外部基準でも確認するため、研究開発分野で一般的なベンチマークが何を測り、どのスコアを KPI としているかを整理する必要があると判断しました。

そこで、HumanEval と SWE-Bench を取り上げ、研究・開発分野で何を指標としてスコアを伸ばそうとしているかを解説します。これらのベンチマークでは、HumanEval は明確な入出力をもつ小粒度タスクに対する関数レベルの正確性を測定し、SWE-Bench は既存リポジトリ上での Issue 修正達成(文脈統合・依存解決・テスト通過)を測定します。現場では前者をユーティリティ/純粋関数の自動実装の置換可能性、後者を既知バグ修正や小〜中規模改修の到達率として読み替えます。本発表では、実際のテストデータを参照しながら両者の評価対象と前提条件を具体的に説明します。

あわせて評価指標にも短く触れます。pass@k は同一課題に対して k 本のコード生成を行い、少なくとも 1 本がテストを通過する確率を示します(例:pass@1 は単発生成の正答率、pass@5 は多様サンプルからの到達率)。SOTA(state of the art) は特定ベンチマーク・評価手順・バージョンにおける当時点の最高到達成績を指します。いずれも評価プロトコルと前提条件への依存性が高いため、比較は同一条件で行う必要があります。

そのうえで、ベンチマークの数値は次の三点で位置づけて読み解きます。第一に、何を前提に何を測っているか(課題の明確さ、必要コンテキスト、依存・ビルド環境、採点方法)を明示します。第二に、どの作業単位に対応するか(例:小粒度の実装、既知 Issue の修正、結合起点の不具合対応)を対応付けます。第三に、影響しやすい成分/しにくい成分を仮説化します。なお、研究分野の「コード精度」は pass@k やテスト合否が中心であり、仕様の曖昧さの解消、非機能要件、ステークホルダー調整、セキュリティやロールバック設計、コードデザイン(責務分割・凝集/結合・API 境界)といった現場要素は評価外になりやすい点を前提にします。本セッションでは、この読み替えを対応表と最小手順として提示し、新しいモデル・ツール・論文に出会った際に、作業単位や手元の指標へトレースする実務的なガイドとして持ち帰っていただきます。

聴講者が得られること
• AI 導入による効果が定量的にどのくらいあるかと、その評価方法
• 研究開発分野での AI エージェントの扱われ方と、どのスコアを KPI として伸ばしているかの整理
• 研究ベンチマークが開発現場でどの程度・どの領域に起用できるかを考え、議論するための視点

5
採択
2026/01/10 13:40〜
Room 204
レギュラー

形式手法特論:コンパイラの「正しさ」は証明できるか?

y_taka_23 チェシャ猫

テーマ

定理証明:複雑なロジックと事実上無限の入力を持つソフトウェアに対して、テストケースの網羅性に依存せず、論理的に挙動を保証する手法およびその実例

想定する参加者層(前提知識)

  • 計算機科学に興味があるが敷居の高さを感じている方
  • 設計と一体化した品質保証に興味がある方
  • 形式手法や定理証明に関する前提知識は仮定しません
  • 特定の CPU 命令セットに関する前提知識は仮定しません
  • 特定のコンパイラバックエンドに関する前提知識は仮定しません
  • 型システムに関する理論的な前提知識は仮定しませんが、何らかの静的型付き言語によるプログラミング経験は前提とします
  • 基本情報技術者試験に出題されるような計算機アーキテクチャの初歩、例えば「メモリとは何か」のような知識は前提とします

トーク概要

本セッションでは、定理証明支援系 Lean を用いたコンパイラの実装技法を解説します。ただしこれは本質的にはコンパイラのトークではありません。頭の痛い複雑なロジックや、うんざりするほど多様な入力データと戦っている、すべてのソフトウェアエンジニアに贈る新しい世界への招待状です。

今日、プログラムを書く際に一緒に単体テストを書くことは、一種のマナーとして広く普及しています。しかし、かつて Dijkstra はこう言いました。「テストではバグの存在を示すことはできても、不在を示すことはできない」つまりテストが成功していたとしても、それはたまたまテストケースが不足していてバグを踏まなかった可能性が否定できない、というのです。一方で、仮に全通りのテストケースを生成してバグの不在を示そうとした場合、組み合わせの爆発により膨大な数のテストが必要になってしまいます。例えば「長さ 3 以下の char の配列を受け取る関数」をテストするだけでも入力パターンは 16,843,009 通り。通常の任意長の配列を受け取る関数ならば文字通り「無限個のテストケース」が必要です。

本セッションで紹介する定理証明は、文字通り、この「無限個のテストケース」を扱うための手法であるといえるでしょう。テストしたい関数の性質を型レベルの制約として表現することで、単体テストのような実行時ではなく静的な型検査時に、かつ「任意の char 配列」のような事実上無限個のテストケースに対して関数の性質を保証できます。

いくつかある定理証明支援系の中でも、Lean は単に証明を記述するだけでなく、実際に動くプログラミング言語であるという面で近年注目を浴びています。一例として、Amazon Web Service では、認可ポリシー記述言語である Cedar の開発と最適化のために、この Lean を採用しています。認可ポリシーエンジンの実装は「ロジックが複雑」「あらゆるパターンに対応する必要がある」「最終結果がぱっと見で分からない」「ミスがあると被害が甚大」という点で、まさに定理証明向きの事例と言えます。また、国内においてもちょうど日本語書籍『ゼロから始める Lean 言語入門』が出版されたばかりで、今 Lean が盛り上がりつつあるのは間違いないでしょう。

本セッションでは、Lean を利用して、自作言語をコンパイルしてシンプルな CPU 上で動かすための「証明付きコンパイラ」を実装します。コンパイラもまた、複雑なロジックと多様な入力が求められるソフトウェアの典型です。ところで、引数と戻り値を持つ個別の関数のテストならともかく、ここで言う「コンパイラの正しさ」とは何でしょう? コンパイルしたプログラムの挙動が正しいこと? ではその「正しい」とはどういう状況か、定義できるでしょうか?

この問いへの答えとして、今回の解説では、コンパイラの性質を「ソース言語の意味論」と「ターゲット言語の意味論」の間をつなぐものとして定式化し、実装したコンパイラが意味論を保存することを証明します。また、コンパイラの挙動を保証するための理論的な解説に加え、実際に動くプログラムを書けるという Lean の特性を活かして、「インタプリタ」「VM」そしてその間をつなぐ「コンパイラ」をそれぞれ実装し、簡単なプログラムをコンパイルして動かす様子もお見せします。

受講にあたって必要なものは、プログラミング経験者であれば普通に知っている程度の知識と、ほんの少しの知的好奇心だけです。定理証明や特定の CPU 命令セットに関する前提知識は要求しませんし、それどころかコンパイラとしては、最適化も行わない、本当に素朴な実装しかしません。むしろ「コンパイラの正しさとは何か?」を題材として、複雑なプログラムの挙動も数学的にきちんと定式化できるのだ、そしてそのための理論や考え方は、他ならぬあなた自身とも無関係の世界ではないのだ、という感動を味わって頂ければと思います。

8