In Types We Trust

Scala ensures that types are used consistently with their declaration, but checks only the name and structure of the types. A type also implies a semantic contract, which is typically expressed in human-language documentation and checked by tests. Can we do better?

In this talk I will propose that we formalize the specification of semantic contracts as statements of predicate logic. I will show how these statements of logic can be used in both property-based unit tests and proofs. I will show you new features of ScalaTest that support this approach.

Required Knowledge

• A basic familiarity of Scala