Correctness.scala
trait Correctness {
// Let’s talk about programs.
type P
// A specification is a predicate on a program.
trait S { def apply (p: P): Boolean }
// We say "p implements s" when a program meets a specification.
def `p implements s` (p: P, s: S) = s (p)
// We shorten this to "p is correct" when a specification is contextually impli…
Keep reading with a 7-day free trial
Subscribe to Type Classes to keep reading this post and get 7 days of free access to the full post archives.