I have released a new version of IsarMathLib. This time there is some new formalized mathematics related to the theorem that two linearly ordered finite sets with the same number of elements are order-isomorphic and the isomorphism is unique. I have written previously on the motivation for this. The theorem was surprisingly tedious to prove and required about 50 lemmas in a couple of theories. Some corner cases were quite bizarre and kōan-like. For example: what is the order automorphism of the empty set? Turns out the empty set is a function, an injection, surjection, bijection and the only order automorphism of itself.

I found that IsarMathLib is traced on the Ohloh site. Ohloh tries to give various metrics on the code for open source projects that it can find on the web. According to Ohloh, IsarMathLib is written mostly in JavaScript and I am a very lousy JavaScript programmer. I guess this is because of the Tiddly Formal Math site template that is included in the IsarMathLib Subversion repository. They do notice that the project has some Haskell code, but also mention OCaml and this is a complete mystery to me. Isar is not on the list of the languages they support, which is not too surprising. This is funny, but may be I should be concerned? What if I am looking for a job and the HR person finds that my programming style is bad and my code is poorly commented, as Ohloh claims? Will I have a chance to explain?

### Like this:

Like Loading...

*Related*

Tags: formalized mathematics, IsarMathLib, weirdmath

This entry was posted on September 27, 2008 at 12:53 am and is filed under announcements, IsarMathLib releases. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

September 27, 2008 at 3:33 am |

I am the one who registered IsarMathLib to Ohloh, sorry if I bothered you. They probably think ROOT.ML is written in OCaml, since, you know, it has .ML extension.

September 27, 2008 at 1:39 pm |

I think it was a good idea to register IsarMathLib. I would have done it myself, if I had known about Ohloh. Maybe one day they will support Isar. I wander if there is a way to straighten up that JavaScript misunderstanding …