Last week I failed to do any work on my website program, as I was taking a look at agda2. Dependent types are awesome!
I was seriously considering whether it would be possible to prove classes such as vectors and matrices in agda, and then generate Eiffel classes from the code. Where agda requires totality, it should be possible to generate preconditions for Eiffel, so as to avoid defensive coding. At least I think so. I didn't follow it up though, as when I checked on in built support for IEEE floating point types (I want double-precision numbers in the vectors and matrices), I found there was none. Maybe I'll take another look at this some time.

In the mean time, this week I'm back on the website, and the image gallery is nearly complete (I've actually got round to worrying about the formatting). Still need to finish the pager and then think about editing facilities.