Codemist Ltd. seems to have released their source code to Codemist Common Lisp and Codemist Standard Lisp. I haven't seen an official anouncement anywhere, but a .tgz and .zip package are both available. Furthermore, in discussion with Rainer Joswig on IRC (#lisp, irc.freenode.org) a few days back, it seemed that the open source release of the Axiom source code was soon approaching as well, which was based on Codemist's Lisps. They also sell a version of Reduce; both Axiom and Reduce are computer algebra systems. However, upon an admittedly cursory inspection of the code included in the CCL archive(s), it appears Axiom is all there! I'm not sure and I'm not authoritative, but it looks like it.

Here's an odd request: can anyone confirm that Xanalys (nee Harlequin, which is now Global Graphics) has officially stopped development and support for MLWorks? Or would know someone at Xanalys I should contact to ask? I recently came across a copy of it and was surprised and pleased to find it, but without a serial number, I can only use it in "Personal Edition" mode, which enforces some memory limits. Since I believe neither Xanalys nor Global Graphics is selling or supporting it any more, I don't think this would be a huge problem. Perhaps one of you readers out there in blogville knows someone who can help me.

In a recent diary entry, Raph mentions:

"Given the obvious usefulness of code, it's tempting to put a virtual machine into the proof checker and proof object file format. A proof can include code when it also includes a proof that the code is correct. Such a proof will also imply that the code is safe, by the way. The checker will verify the proof of the code first, then assuming it passes, just run it. The output can be entered into the database of statements proved correct, just as if it had been spit out from an inference rule."

Sounds like proof-carrying code, although Raph's approach has sort of switched this around (perhaps this is a purely semantic point); his idea is possibly more adequately described as "code-carrying proofs". Raph, have you looked at PCC? Any thoughts?

For whatever it's worth, I had a big interest in PCC not too long ago, and I still believe it has merit, but it seems to be bogged down in the security research world. One of my more fanciful flights while at OpenCola involved PCC, mobile code, and capabilities (of course, I was mostly thinking all in E too, along with some Haskell at the time), which I thought would all go very well with each other. Indeed, PCC has been used in the field of mobile code more or less since it's first proof-of-concept. The farthest I got was just in some conversation with co-workers. I didn't have an opportunity to start an actual project around it.

Early morning funny straight from the Bristol-San Francisco comedy pipeline:


[04:18] <dnm> I have Corn Flakes.
[04:18] <dnm> Hell yes.
[04:18] <dnm> For the first time in like four months
[04:19] <dnm> I can have cereal for breakfast.
[04:19] <rik> dmn: I have porn flakes. they're like cornflakes, but with specific shapes.


Playing around with various TeX things. I am not terribly impressed with Maple 7's default LaTeX export features, given that the output relies on some specific sylesheets (which they do give you). Running a quick PDFLaTeX on the generated LaTeX results in nothing spectacular and really quite odd looking in places. Of course, there's nothing stopping me from tweaking the output source.

Also futzing around with Metamath after seeing Raph compare and contrast it to HOL. I began playing with HOL a while back after Bram and I talked about it passingly at Stacey's Bookstore (I run into him there a lot).

Thinking deeply about small p philosophy. Please excuse the pensive, silent mood if you happen to be around me in person.

Happy Birthday to my ex-flatmate Paul Baranowski, programmer of fortune.

My contract with Cloudmark ended earlier this month, so I'm available for contracts, consulting, and more. Contact me if you're interested.

I'm busy resurrecting old projects, including beepcore-ruby, unfortunate unkempt scarecrow of my docket of geek goals. However, it picked up a few new interested people and the mailing lists are now up. Also, a barebones web site is now functioning. I'm working on putting out the initial design docs, which themselves are presently undergoing revision from the last time I really thought about the design of this project, roughly a little more than a year ago, now. One benefit of this is that there a number of BEEP Core implementations around now compared to then, so there's more to study from our neighbors.

Also, now occasionally spend too much time futzing with my Ryze page. Ryze can get addicting.

'Mile High Club' Forces Airplane Refit

"The $200 million Airbus A340-600, which was introduced several weeks ago, has a "mother and baby room" with a plastic table meant for changing diapers. But passengers have destroyed them by using them for love making."

No comment.

[23:59] <AccordionGuy> Boring is the new black.