skaller wrote: > Yes, but mere statement of the laws would be useful, > even if they can't be proven and we falsely claim > they're all axioms .. might have been better to call > them 'laws' than axioms, since that doesn't try > to separate axioms from theorems. > In which case, I would go with 'obligation' rather than law or axiom.
As far as proofs in Felix, take a close look at Concoqtion (Google it). It integrates Coq into Ocaml in an interesting way. Should help with ideas of how to integrate Proofs in Felix. > The idea here isn't proving program, or even typeclass instance > correctness, but rather simply proving some typeclass 'axioms' > are theorems. Hopefully this reduces the workload to get > *some* proof capability into Felix. > Right - this is similar to the approach Concoqtion takes. Jacques ------------------------------------------------------------------------- Using Tomcat but need to do more? Need to support web services, security? Get stuff done quickly with pre-integrated technology to make your job easier. Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642 _______________________________________________ Felix-language mailing list Felix-language@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/felix-language
