Coq Party - rfなブログ

11/27 に、Coq Partyに参加してきました。

資料などはこちら。

エンジニア・ミーツ・Coq
- すぐ分かる形式手法
  - 形式手法とは？
    - 品質の高いソフトウェアを作るための科学的な仕様記述・検証手法
      - 仕様化の正しさは終盤のシステムテストまで分からない
        
        結合テストでバグが「こんにちは！」
        
        手戻りコストがとても大きい
      - V字モデルは横軸工程、縦軸は「開発の詳細さのレベル」
  - ソフトウェア開発の不具合の半数は上流工程
    - その半分は下流工程まで見つからない
    - 上流時点で「厳密で、間違い、漏れ、抜け、矛盾の無い仕様」が必要
      - 仕様は自然言語で書かれているため、あいまい
        
        or/xor 問題や、if/iff 問題など
        
        自然言語ではなく、形式的な仕様記述が必要
  - 形式手法
    - 「形式仕様記述言語」によって仕様(形式仕様)を記述し、設計や検証を行う
      - 数学ベースの厳密な定義
      - 形式仕様は仕様の記述の形式化
        
        プログラムではない (≒実行できない)
    - 仕様のシミュレーションやコード生成などが出来るツールがある
      - Coqもその中の一つ (定理証明支援)
  - メリット
    - 自然言語より厳密
    - 上流工程で仕様に対する検証が可能
    - 仕様不具合の早期発見
    - 「証明」などの、高い検証能力
  - デメリット
    - 学習コスト
    - 不具合が完全になくなるわけではない
  - 自然言語とプログラムの中間
  - 各工程で仕様等の検証が可能
  - 形式仕様について完全な検証を行いたい場合、証明を行うことができる
    - テストするだけでは、テストケースから外れたものについては検証しきれない
    - 記述した形式仕様に証明を与えることが出来れば、その仕様は「数学的に正しい」ことが保証される
    - 証明された使用から自動生成されたプログラムは、仕様通りの動作をすることが「証明されて」いる
    - 一般に証明はテストに比べ難しいので、コスト高になるといわれている
    - Coq では、「仕様記述」「定理や補題の付与」「証明」「コード生成」
  - まとめ
    - 仕様をどう記述するかはとても大事
    - 形式手法なら厳密に矛盾なく仕様が記述できる
    - 形式仕様を証明すると、テストよりもスゴイ検証になる
- エンジニア・ミーツ・Coq
  - ProofCafe
    - 名古屋市内のカフェ「どえりゃあ」
      - お見合い席の隣で Coq やったり
      - おしゃれな食事の隣で Coq やったり
  - 定理証明って面白い！
    - パズルゲームみたい！
  - 普通のプログラムでも証明使えそうじゃね？
    - 普段の業務におけるプログラミングでも、証明が役立ちそうな場合は多い
  - 「ProofCafe で Coq を知ったので、会社で普及させようとしてみた」
    - 流石に職場ですぐに使うのは難しい
    - 「なにで出せますか？」「OCaml です」「OCaml 難しいです＞＜」
  - 職場で Coq を普及させるときの難しさ
    - 「1. OCaml ライクな構文」
    - 「2. 証明とプログラミングのギャップ」
    - 「3. 命題を考えるのが大変」
    - 「4. 数学の知識がたりない」
- 最後に
  - これから形式手法や定理証明などの力が必要になってきそうな予感
  - 新しい技術を積極的に試すのは大事
  - Coq は触れてて楽しいし、証明できると嬉しい
- 没ネタ
  - 「坊や一緒に定理証明をしようよ！」「おとーーさん！おとーさん！魔王が Coq を進めてくるよ！」

ProofCafe で学んだこと
- なぜ Coq を勉強しているのか
  - 今井さんと出会ったから
    - 「λ！λ！λ！」
- Scala
  - 緩い感じの関数型言語
  - 「λ^3」(λキューブ)
    - 証明が出来るよ！(Coq)
- ProofCafe 1回
  - リストの操作とか、その性質の証明とか
  - 「Coq 楽しい」
- ProofCafe 2回　CPDT 2章
  - 難しいが、全体を俯瞰しているだけなので、わかんなくてもいいよ
  - 3章から頑張ろう
  - CPDT翻訳
- ProofCafe 3回　CPDT 3章
  - CPDTに「みなさんお気付きのとおりこれはラムダ計算の構文です。HOASです。さあこれをCoqでも使いましょう」と書いてあって、前提知識が足りないことに気づく
  - 難しい・・・
- ProofCafe 4回　ハンズオン
  - 再度Listを定義して、関数書いて好きな定理を証明しよう
  - ペアプル！
- ProofCafe 5,6回　CPDT 4章
  - Coq CheatSeet
- tactic
  - change tactic 便利っぽい
  - 「transitivity が好き」
  - 「injection より inversionのほうがいい」
  - 「今人気の tactic 出そう」
  - 「info auto で auto でやった tactic を出せる」
  - 「俺のスキなタクティクス elim,ring,omega,inversion,transivity,assert」
  - あなぷるからひろってきたタクティクスの使用数ランキング
- プログラマのためのCoq - zyxwvの日記
- 証明の過程が知りたい
  - バージョン管理しながらやるといい感じ
- 初めての Coq

Haskell の Data.Map のバグを見たら Coq を 12,000 行書いてしまった話
- 「形式化おたくになろう！」
- バランス木が崩れちゃったバグ
  - パラメータの組み合わせが違うと、バランスが崩れる
- パラメータを 5 -> 4 にしてなおったよってチケットが閉じられた
  - ほんとに大丈夫？
- アルゴリズムのバグ
  - バランスの定義して、改善したアルゴリズムがバランスすることを証明
    - 中にいれば大丈夫 + 外だと崩れる
      - 外は、崩れる木が存在することを示す (手でいいや)
      - 中は、大変なので Coq で証明
  - Word を使うと 12900 行でもスライド1枚で収まる
- psatz 便利
  - A <= B を A <= C と C <= B にするのを自動で
- 証明にインデントを付けるのは大事
  - 場合分けとか
- Coq これやっとくといいかも
  - Coq のドキュメントが手元にあるといい
    - inria よく落ちる
    - mzp さんがミラーサイトを作っている
  - Coq が自動で作った名前は使わない方がいい
    - バージョン上がると名前変わったり・・・
      - バージョン明記して諦めるという手が・・・
        
        古いバージョンも持っておけと・・・
        
        業務だと開発環境をとっておくことも多い
  - nsatz 便利
  - Ltac 書けるようになった方がいいんじゃないか
- プログラムに対して 100倍くらい証明にかかる
  - プログラム側 120行に対し、証明12000行とか
- intuition 便利

定理証明器 Coq と証明付き DSL (FM勉強会の話と Coq を DSL に使う話)
- Coq を学ぶべき理由
  - テストで発見できるのは間違いだけ
    - 正しいことは保証できない
  - 網羅性のあるテスト書くの大変
  - オレオレ言語に信頼性はあるのか
- Formal Methods Forum
  - Google グループ
  - もとは Scala-be の Step by Step Scala勉強会
  - 無料の形式手法講習会がなかった
    - やりたいね
  - 個人的には定理証明系の勉強会がしたかった
    - あんまり上流工程に興味ないし・・・
  - Alloy と Coq が中心
  - 関連勉強会
    - TAPL, Stebe Awodey 読書会
- DSL
  - 特定分野のタスクのために作られた言語
  - 自然言語より簡潔かつ厳密に記述可能
  - 正しさをどう担保するか
    - DSL で書かれたものの正しさ、DSL 自体の正しさ
  - Ott 証明木を書くと、Coq と LaTeX と Isabell に変換してくれる
    - http://www.cl.cam.ac.uk/~pes20/ott/
  - 金融商品 DSL
    - 自然言語でなく Python を使う提案
      - 何故 Python？
      - 型付き関数型言語使えば、型検査で DSL の安全性を担保可能
  - 認可・監査論理
  - Coq で証明されたC言語コンパイラ
    - 生成されたコードは元のCコードと等価であることを証明
  - 外部 DSL と内部 DSL
    - 外部 DSL
      - どうせなら Coq とかを使って言語の正しさを証明したい　
    - 内部 DSL
      - Coq は実は DSL 向いているのでは
  - DSL Host Language としての Coq
    - ユーザ定義の記述を定義できる
      - Notation
        
        定義と一緒に where で記法を定義できる
        
        Haskell の do 記法も書ける
        
        .. で繰り返しのあるパターンを書ける
        
        予約後の上書きに注意
      - LTac
        
        外部呼び出しもできる (external ...)
        
        脆弱性注意
        
        気をつけないと矛盾を持ち込んで Falso みたいになるかも

Coq extraction機構の概要
- Extraction
  - Coqからプログラミング言語への自動変換
    - OCaml, Haskell, Scheme
    - 「Scheme だとこんな感じです。括弧がいっぱいありますね」
  - 検証対象が直接実行形式になる
  - 対象言語の中で局所的に Coq を利用できる
    - 段階的に利用できる
  - 全部を Coq でやるのは非現実的だけど、対象言語と組み合わせるととても良い
  - 他の検証機のプログラム生成
    - Agda -> Haskell
    - Isabelle/HOL -> OCaml, Haskell, Scheme, Scala (実験的)
    - ACL2 -> ？
    - NUPRL -> ？
  - Coq -> X言語を増やしたい
    - Coq ソースコード内 plugins/extraction (8.3) (8.2だと contrib/extract)
  - Extraction の実装を Coq で書いて Extract とか
  - Extraction 周りは夢がひろがりんぐ
  - 「Coq は使いこなせるけど OCaml はちょっと，という皆さんが Extraction を書けて便利だと思います」

From Coq to Ruby Coq から Ruby へ
- Extraction のうれしさ
  - Coq が使える ← うれしい
  - どの言語の勉強会でも Coq の話が出来る
  - 証明したコードが他の言語から使える
- 証明駆動には、Extraction が不可欠
- Ruby の特徴
  - 型がない
    - Extraction 先としては、型がない方が楽
  - ラムダ式がある
  - 関数と変数で名前空間が分かれている
  - パターンマッチがない
- Ruby に Extraction
  - 「ハッピーですね」「ハッピーかなぁ・・・」「ハッピーですよ」
  - lambda がいっぱい！
  - 美しいコードを出力しようと思わなければ、結構簡単にできる
- 抽出対象として適している言語
  - 型がない・動的型付け
  - GCがある
  - ラムダ式
    - なくてもオブジェクトでなんとか
  - パターンマッチ・バリアントがある
  - 関数と変数で名前空間が分かれていない

家に帰ったらExtraction to x を書いてみよう (Coq2Clojure)
- Coq (Gallina) の特徴
  - OCamlっぽい関数型言語
  - 関数は全てカリーか
  - 関数と変数の名前空間が同じ (LispだとLisp-1)
  - CoInductiveで遅延評価
- Scheme
  - 代数的データ型はない
  - 関数はカリー化されない
  - Lisp-1
  - 安心の末尾再帰呼び出し最適化
  - GCあるよ
    - もはや当たり前になってメリットに挙げるのを忘れられやすいGC
      - でもなかったらとても大変
  - Extractionで幾つかのマクロを作る
- ClojureへのExtraction
  - Scheme ベース
- Ruby
  - カリー化なし
    - 関数はラムダ式の入れ子で
  - メソッドと変数の名前空間が別 (Lisp-2)
  - 代数的データ型は配列で表現
  - 再起用にYコンビネータを自作
- 型のある言語
- 依存型のない言語にCoqのやり方を理解させるのは難しいらしい
  - OCamlだと Obj.magic, HaskellだとunsafeCoerce してる
- 対象にしやすそうな言語
  - JavaScript
    - Lisp-1
    - カリー化、遅延評価、代数的データ型まわりは自分で
    - 関数型な人はreturnではまるかも
  - Python
    - Lisp-1
    - インデントを上手く付けるのが面倒かも
    - returnあった気がする
  - Common Lisp
    - Lisp-2
    - 基本的にはマクロで乗り切れるはず
- 動的型付け言語こそ証明を！

懇親会
- あなぷる課金できるようにしようとか
  - あなぷろになろう！
- Coq はチューリング完全にはならない
  - 停止しない関数書けないし
  - semi-recursion？

帰り
- 大学が最寄りの駅から徒歩60分って、ぇ・・・