There's a post by Neil Tennant on The Role of Formalization on the FOM list, where he says:
> This reminded meThis is exactly right, and this is what Raph's proof exchange format has to get right if it is really to break out the "formalised mathematics" ghetto.
> of an anecdote of a student of axiomatic set theory who insisted in
> writing all of his proofs for homework exercises in a extremely
> rigorous fashion. All of his proofs were symbolic and with the
> appropriate software these proofs could probably have been checked by a
> computer. The grader was a bit confused as to what to do with these
> proofs since they were correct and very rigorous but it was not really
> what was expected from him. After a while, the professor and the grader
> recognized the fact that it was in some sense admirable that he wrote
> his proofs so formally, but requested him to start writing his proofs
> at a higher level of abstraction, which was more appropriate for
> human-readability.Perhaps readability by human beings is best ensured not so much by "writing ... proofs at a higher level of abstraction", as by endeavouring always to use such formalisms as permit one to give perfectly formal proofs that are more nearly *homologous* to the patterns of informal reasoning that human mathematicians typically employ.
...
IMHO the formalization of mathematics, if it is too enable machine-checking as well as readability-by-human-beings, is going to need much more careful design of its basic rules of inference. We need to deal not only with connectives, quantifiers and the identity sign, but also directly with the various mathematical primitives. By "mathematical primitives" here I mean not just the epsilon in a Bourbaki-style axiomatization of a given branch of mathematics in ZFC. I mean, rather, the notions that are treated as linguistically primitive in the usual course of ordinary mathematical talk.
Intelligence Post
Jean-Paul Ney [fr], a freelance French TV field journalist, has started a slashdot-alike (PHP Nuke based) intelligence/terrorism news portal, Intelligence Post, which I recommend. It's got its teething problems (eg. it has an RSS aggregator whose choices are all Linux/BSD sites, not really on target for most of its audience; a few bugs, eg. number of comments doesn't display correctly), but the site does an excellent job of selecting and bringing together news articles within its remit: I would have missed two very interesting stories about Iran had I not found this site. There's a few folk here I know will be interested in this site, hence the recommendation.
The two Iran items I mentioned above are:
Felix on the Google IPO
Felix Salmon has a really excellent analysis of the Google IPO.
Recentlog
cTaylor: Your ideas for a grammar checking engine look nice, and you seem to be going about it in the right way. I wouldn't usually say something so trivial, but since you think you might be driven insane by your project...
crhodes: Protocol oriented programming I've never heard of before (I'm guessing you didn't invent it), but the way you put it fits in nicely with modern ideas in formal specifications. There's some interest in the idea that you can give description languages for protocols that are logic programming languages such that the specification determines the execution, (ie. the way PROLOG is supposed to work).
mmangino: De Paul university, eh? A doctorate-brother of mine, Corin Pitcher, works there. Maybe an interesting contact for you? He does both the difficult theory and the messy practice of computer science, and he has a background in mathematics.