プログラムの型とデバッグ手法を聞いてきた！

昨日（１０月２０日）NIIの市民講座
情報学最前線
「正しいプログラムを簡単に書くには？プログラムの型とそのデバッグ手法」
を聞いてきた！ので、その内容をメモメモ

---

・正しいプログラムは何で必要か
　いろんなところでプログラムが使われている
　　→正しいプログラムを書こうという努力

・プログラムとはどんなものか？
　速く書けるときもあるが・・・

・プログラムとは何か
　コンピューターへの指令・指示書
　例：１～１０までたしてください→あいまい

・プログラム：明確な手順を指定した指令

・プログラムはどう実行されるか
　　１＋１０＋２＊３
　　　　字句解析（じくかいせき）：トークンの列
　　　　構文解析：トークンの列→（どことどこがくっついているのか）→抽象構文木
　　　　各種変換・最適化・コード生成：抽象構文木→いろいろ→機械語
　　　　機械語を実行する＝１７


　※字句解析、構文解析はツール（lex,yacc）。
　　構文解析器は古くからあるが、今も研究
　　「LR構文解析の原理」大堀淳

・正しいプログラムとは何か
　　・コンピューターが解釈できる
　　　　→実行は出来る
　　・人が思ったとおりに動作する
　　　　→意図どおりに書くのは難しい

・プログラムの正しさを、どう高めるか？
　　・データの種類に注目して、書けるプログラムに制限を設ける

・データの種類：型
　　→型を使って制限する
　　　　：動作を予期しないプログラムをのぞくことが出来る
　いつ型を検査するか
　　１．静的型付け：実行前検査
　　２．動的型付け：実行時検査

　※値の性質まで入った型： LiquidHaskell

・型の難しさ
　修正→型エラーのデバッグ手法

　本質的な難しさ
　　どれが正しいかは自動的には決められない

　型エラーのデバッグ手法
　　エラーに関係している：型エラースライス
　　対話的に：対話的型エラーデバッガ
　　可能性の高い：原因箇所推定

・研究の話（宣伝）
　機能を再利用

・型以外の手法
　　テスト
　　性質の検証

・テスト
　　研究：テスト例自動生成
　　　→自動生成をどうするか：ランダム、小さいものから全通り

・性質の検証
　　性質が満たされるか証明する
　　　→自動定理証明：ここ１０年ほどホットトピック

・本講座で話したこと
　プログラム：明確な指令
　プログラムの正しさ
　正しさを高める「型」
　型以外：テスト・証明

・プログラムを書くには？
　プログラミングの学びかた：コースとかあふれている
　　　Gacco はじめてのP
　競技プログラミング、プログラミングコンテスト
　　　ICFP　プログラミングコンテスト

Q&A
・静的と動的の型付け、どっちがいい
　→大規模は静的、ネットでの処理・外部との受け渡しは動的
　　１回実行すればいいのも動的で

・なんで似たような言語が出てくるの？
　言語を作るのが好きだから

・ツールはどんなの？
　emacs

・生産効率的な点からコメント
　型を使う：型がひとつのドキュメント→あがっている
　ソフトウェア工学で研究しているので、そちらのほうを見て