# Thoughs on Theory.pm

`(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).