title: 形式手法を広めるには
author:  河野真治 <br> 比嘉健太
profile: 琉球大学工学部情報工学科
lang: Japanese

# Agenda
* 大学ではどんなことをやっているか(講義, イベント, 研究)
* 講義などでつまづくポイント
* つまづきの解決策

# 講義で紹介する形式手法
* model checking 的なアプローチ
* 証明的なアプローチ

# model checking 的なアプローチ
* Operationg System の講義
* Process/Thread Scheduling を考えた時に
* Dead Lock を起こすような Scheduling を実際に書いて実行させる
* Java Path Finder で Thread の実行順序を網羅的に実行する

# 証明的なアプローチ
* ソフトウェア工学 の講義
* 集合, 論理, 関数, 自然演繹による証明
* 型システム, Curry-Howard Isomorphism を通して Haskell, Agda で証明
* Haskell : 自然演繹と lambda calculus
* Agda    : Data type に対する証明 (Product, Sum, List, Functor, Monad ...)
* Agda    : SystemT を使った自然数に対する演算の証明

# Agda による証明を解説した例
* Open Source Conference
* ソフトウェア工学で学んだ Agda の使い方を発表
* Agda で SystemT の Nat の加法の交換法則を解説
* ほとんどが定義の解説に時間を取られてしまう

# 圏によるプログラムの形式化
* プログラムの変更を Monad で表す
* プログラムの変更時に変更前のプログラムも残したまま変更する
* 全てのバージョンのプログラムを同時に実行できる
* デバッグやテストと組み合せることでバグ
* 実行系と検証系を同時に走らせることもできる

# 学習コスト
* 論理, 自然演繹 -> Haskell -> Agda
* それぞれのステップに壁がある
* 自然演繹では解けるけれど lambda term で書き直す
* Haskell では定義できるけれど Agda で証明できない

# つまづくポイント
* Haskell -> Agda の壁を考える
* コードを書いてる人なら型を合わせることは分かる
* 型によって証明を書くことに繋げるには?
    * プログラムと論理の対応を把握してもらう必要がある
    * どうしたら把握してもらえるか?

# つまづきをどう解決するか
* 書き続ける
* 論理とプログラムの対応を見えるようにする
    * Agda は対話的に項を書き換えることができる
    * どこでつまづいても情報が手に入るようにしたい
    * 対話的に情報を引き出す手段そのものを学ぶ

<style>
.slide.cover H2 {
    margin-top:72px;
    font-size:72px;
}
.slide.cover H3#author {
    margin-top:72px;
    font-size:42px;
}
</style>

<!-- vim: set filetype=markdown.slide: -->