Agdaで画面づくり、は結構いけると思う話
http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/
でポスター発表してきました。ポスター（実態はスライド）も
http://www.slideshare.net/ShujiKinoshita/ppl2015-uivalidationfull
に置いてますが、それだけだと何のことかわからない部分も多いので補足しときます。
主に、PPLにいたけど同じ時間にポスター発表していて、聞いてない人向けです。
- 問題
- その問題は解決するに値すると思う理由
- その問題の解決方法
- 解決できそうだと予想する根拠
に分けて話します。
【問題】
- 残念なぐらい使いにくいソフトウェアとかサービスがたくさんある
【その問題は解決するに値すると思う理由】
- ソフトウェアやシステム、サービス、というのはほとんどの人間が日常的に触れるもの。
- 業務でパソコン等々の電子機器を使うなら、画面とにらめっこする人は多い
- クリティカルなシステム（例えば原発内で稼働するソフトウェアとか）ではオペミスが致命的なことになる。オペレーションがうまくいく、人間はストレスを感じず操作できる（つまり、画面は妥当である）、ということも何らかの形で保証したい。
- クリティカルでないシステムでも、日常的に触れるシステムが使いにくい、というのは問題。そのストレス指数みたいなものが明確に数値化されていないから、問題ではないと思っているだけで、実はものすごく問題。ユーザのイライラの総和は侮るべからず。
【その問題の解決方法】
- ソフトウェアの画面記述言語としてAgdaを使う。要するに、Agdaコードから画面用コードを自動生成するジェネレータというかコンパイラをつくる。
- Agdaの「プログラムとその性質の証明をあわせて書ける」という性質を利用して、画面定義と、その妥当性の確認を一緒に書く
【解決できそうだと予想する根拠】
- ソフトウェア一般の妥当性確認は難しいが、画面の妥当性に限れば、既存研究がたくさんある。主にユーザ中心設計（UCD）やUI/UXデザインの諸分野。ただし、形式化するという話はあまりないので、それをやる、ということ
- 形式化はできそう。やり方はいろいろ考えられるが、とにかくドキュメントの成果物を（あまり構造を考えずに）Agda上にのせるだけでも、「画面が変更になったらドキュメントも変更しないとダメ」という程度の簡単な型検査には落とせると思われる
- あるいは、「主な業務は3クリック以内で終わる」だとか、「主な業務は10秒以内に終わる」というようなことはAgdaで記述、証明できそう。
- システムの妥当性確認の分野でよく使われる、アシュランスケースをAgda上で形式的に記述できることは知られている
- Agdaで書いたアシュランスケースからXMLを出力して、それをEclipse GMFでグラフィカルに表現するツールは既にある。つまり、Agda to HTMLは技術的には（Agdaの実装をいじれば）そんなに難しくはない。
といった感じですが、もう少し面白いと思ってもらうには動くデモがないとダメだなあと痛感しました。動くデモができたら、またどこかで喋りますのでよろしくお願いします。全国1000万もとい1000人ぐらいのAgdaユーザの皆様よろしくお願いします。
