正しい Scala プログラムの書き方

Scala は、そのままでもその関数型である性質から正しいプログラムを書くための設計ツールを与えてくれる。例えば、型の多相性、高階関数、不変性などが挙げられる。さらに、多くのテストフレームワークもあり、それらはバグの一部を検出してくれる。しかし、もっと頑張るとバグの不在を証明することが可能だ。

このトークでは、Scala コードをテストして、論理的に解析し、正確さを証明するための技法を解説する。プログラムに対する普遍性 (universal property) を定義し、検証する方法をみていく。また、このトークでは従来とは全く違った方法で Scala コードを書く方法もみてみる。