Metablog

The Avacore CoreControl, sometimes known as The Glove, is an extremely neat idea. It regulates the core temperature of your body by directly cooling your blood. It turns out that by keeping your core temperature in the normal range, you can exercise a lot longer and more effectively than you could otherwise. I always wanted one because I play a lot of DDR, and I always get tired (and sweaty) more quickly than I get bored.

So for a while I thought about trying to build one using the principles in the linked article. It’s actually a very simple device, mechanically. All you have to is make a chamber that your hand fits in along with a source of cold, like an ice pack. You make the chamber airtight, with a simple seal around your wrist. Then you pull a slight vacuum in the chamber. Just enough to bring all the blood in your palm to the surface. The seal doesn’t have to be all that tight. Then you leave it for a minute or so while your blood circulates.

The vacuum counteracts the vasoconstriction effect that naturally happens when your skin encounters cold, allowing the heat to be transferred out much more efficiently than without a vacuum.

But I never did build it. I’m not a very mechanically-minded person. I’m much more of a programmer than an engineer. So when I discovered a few days ago that the product had finally come to market (a few years ago), I was pretty excited. How much would I spend on it? Oh, probably a few hundred dollars.

How much does it cost? They don’t say on their website. So I called them. $3000. Wow. So I told them, you know, you should consider offering a set of plans for hobbyists, who are most likely not among your potential customers at that price. (Nor are your potential customers likely to be frugal or nerdy enough to build one themselves.)

The fucking sales lady hung up on me. Not even a “no thanks”.

Fuck Avacore.

If anyone reading this has any talent for building things, how about let’s make some do-it-yourself instructions and post them online? You know, using basic tools and materials you can get from a general hardware store.

I looked into software piano synths a while back, and by far the neatest one was Pianoteq. Amazingly realistic and responsive, and ideal for integration into the MIDI editor I was writing at the time. The only problem with it was that the sound wasn’t quite calibrated correctly. It lacked a little something, hard to put one’s finger one. Well, with their new major version, I now fully approve of the sound, and may in fact buy the product at some point. (I may get a cracked version before then, and then go ahead and buy it if I ever release my project.)

Of course, me using this would mean that I would have to actually start working on this project again, which is unlikely to happen. There are many projects vying for my attention. (Some more productive than others.)

I’ve been doing a lot of mathy things recently, and one of them has been playing with Metamath, which is step by step formalizing a whole bunch of mathematics. You can see what real numbers really are, how recursion and induction can be defined using only basic set theory, what a function really is, and a million other neat things. It has proofs for all of its theorems that can be verified by a very simple program, or by hand if you like. It’s just a whole bunch of substituting A for B and matching.

The only problem with it is that it’s kind of low-level. It’s hard to follow the proofs and even sometimes the definitions. Now, on the one hand, it’s probably good to become more fluent in formal mathematical language if you want to learn a lot of math. But on the other hand, part of the difficulty I was encountering was entirely avoidable, due to not including enough information about the proof when it’s displayed. In particular, to know what substitution is being made at any given point, you have to open the theorem being used at that step, and then go back to the proof. If the theorem is quite large, you might have to go back and forth quite a bit to get it in your head enough to understand what’s going on. And further, for very long equations, it can be completely impossible to do this in your head.

So I made it all happen on the screen, right there in front of you. Proofs still aren’t easy to follow, but they’re quite a bit easier than they were. Perhaps as easy as they’re going to get with Metamath. We’ll see if I get any better at reading them now. (By the way, this is done along with shrinking the site quite a bit by having it all done in javascript.)

Unfortunately, I don’t currently replicate all of the features of the Metamath site, since that would be hard and kind of boring. So you need to really start here, and then type in http://pdf23ds.net/projects/Metamath/theory-name.htm when you have a theorem whose proof you want to follow.

I invite your comments.

Hi, google!

And hi, searcher! If you’re looking for a .NET or C# or VB version (really, just the output part) of the Rats! PEG parser, I can probably help! I have written such a thing, and could be persuaded to assist with its use. It isn’t in the main distribution of Rats!, for various reasons, though could be in the future if there’s any demand for it. There is a Bazaar repository with my changes here (though this might not be the latest–check with me).

Check out all my awesome branches. To get one, download Bazaar, a pretty good revision control system, and type in (for example)

bzr branch http://pdf23ds.net/bzr/Common/trunk Common

I’ve put a lot of my source in there, including everything needed to build (if you dare) Lojgloss. Lots of projects depend on another project. Specifically, most projects depend on Common.

Of course, I can’t guarantee that anything will build or what-have-you. Assume GPL unless otherwise notified. (I don’t really like the GPL, and I’ll put something under a BSD license pretty easily, but there are a couple things I want GPL’d.)

If by some amazing chance you actually want to send me a patch, well, you have my e-mail. And I want to keep the copyright on all my code, so any changes you want me to include must have the copyright assigned to me or the public domain.

All this is a result of my finally getting out of SVN, whose limitations were getting annoying.

I have released a new version of my dynamic compressor with a nicer algorithm. It’s currently in a standalone program version, but I’m planning to release an Audacity plugin version as well.

Update: I’ve released the Audacity version too, which is much faster than before.

Computer science question. What would it take to make a language to describe both an interpreter and a compiler for an arbitrary language? So that you could have one program that takes the description of the target language and interprets that language, and have another program that compiles the target language? If such a specification language were possible, would writing compilers/interpreters in it be practically possible, and if so, how easy? I’m surprised that googling didn’t turn anything up along these lines.

There are languages where most implementations support interpretation and compiling, like Common Lisp, but in general it seems to be the exception.

What is the philosophical difference between interpretation and compiling? How would it be best characterized?

If you’re trying to get logged into another machine, and you put in some bad credentials, but Windows doesn’t ask you again for other credentials, saying “access is denied” or something, then go to your Services (Control Panel \ Administrative Tools \ Services) and restart the Workstation service. Try again, and Windows should ask you for your password again.

Keywords: user name, password, prompt, SMB, filesharing, cached credentials, network, log in problem, log on, security, access denied

I got an Ipod nano last Christmas. I didn’t use it. Well, I finally got around to fixing some problems with my dynamic compressor so I can my classical music on there the way I like it, and extracting the contents of my old linux hard drive (which has been in my machine for a long time, but with its contents inaccessible) with lots of my mp3s on it, and getting a large backup drive to store everything on, and I think I’m almost ready to start using the damn thing. What a lot of work it is!

So I plug it in, and it doesn’t come on. No big surprise—the battery’s dead. I wait two hours. Nope, still dead. I look up how to reset the thing, try it, no results. I’m not seeing anything at all on the LCD screen. Not even the “recharging the graphic” battery you’re supposed to see. Well that’s just great.

So, two days pass. I take a look at the Ipod. Oh, look, it’s on. Interesting. Battery still dead, but at least showing a menu. Not connecting to ITunes, but it’s on.

Oh, look. Now it’s not.

Hmm. This is going to take some work.

Lack of posting due to depression, stress, and working on projects (Lojban translation, Isabelle theorem prover, dynamic compressor) rather than posting. The dynamic compressor’s about ready to release, once I get around to it. I have it as a standalone tool now that does batch processing and is much faster and more memory-efficient (well, except for the fixed overhead of .NET) than the old one.

I’ve decided it might be neat to write a compiler, so I’m going to try writing a lisp compiler, from the ground up. I’m going to start from assembly language, and write my own assembler, and work my way up, building more abstractions and more safety into the assembler until eventually it becomes more of a compiler, and more features into the compiler until I get happy with it. It’ll be self-hosting all-the-while, and probably more-or-less impossible to port to another architecture. Not sure about the platform aspect, though. It won’t be Common Lisp, because that sucks, but it’ll be something along those lines. Most of the same features, none of the all-caps, silly-names weirdness. Probably a number of conventions taken from Java/C#/etc. since that’s what languages are doing nowadays. That is, if I get that far with it.

In the meanwhile, I’m terribly depressed. I was on Lamictal, which was helping quite a lot, but after about 5 weeks of treatment I got a tiny little rash, which apparently can be a first sign of a more serious, deadly rash. My doctor took me off it immediately, which I think was overly conservative. So for the past week I’ve been off my rocker. We’ll see tomorrow if he gets me on something else that will help.

In related news, I am still single.