(ref: http://svn.openfoundry.org/pugs/docs/notes/theory.pod)

> theory Ring{::R} { > multi infix:<+> (R, R --> R) {...} > multi prefix:<-> (R --> R) {...} > multi infix:<-> (R $x, R $y --> R) { $x + (-$y) } > multi infix:<*> (R, R --> R) {...} > # only technically required to handle 0 and 1 > multi coerce:<as> (Int --> R) {...} > } > > This says that in order for a type R to be a ring, it must > supply these operations. The operations are necessary but > not sufficient to be a ring; you also have to obey some > algebraic laws (which are, in general, unverifiable > programmatically), for instance, associativity over > addition: C<(a + b) + c == a + (b + c)>.

`I started thinking about the "in general, unverifiable programmatically"`

`bit. While obviously true, perhaps we can get closer than just leaving`

`them as comments. It should be possible to associate a`

`unit-test-generator with the theory, so I can say:`

theory Ring(::R) { ... axiom associative(R ($a, $b, $b)) { is_true( ((a+b)+c) - (a+(b+c)) eqv R(0) ); } ... }

`And then say "for type T, please generate 1000 random tests of T using`

`axioms of Ring".`

`In an ultra-slow debug mode, the aximons could be propagated as post`

`conditions on every public mutator of T, so that we test them`

`continuously in a running application (or tes suite).`