This project (as an offshoot of numerical haskell) has the following goals
-
formalize the abstractions / ideas articulated in the numerical haskell library. For now this is mostly centered around the underlying address translation machinery, but this is likely to expand to showing equivalence of algorithms built on top.
-
experiment with the different modeling styles of proving
-
figure out what necessary and sufficient "laws" instances of the numerical haskell type classes need to adhere to.
-
eventually formalize actual applied math algorithms!