This summer, I'm participating in Google's Summer of Code, attached to the NetBSD project and working on fixing certain misfeatures of the software RAID driver — more details on which later.
Various other SoCers have declared their intention of keeping a weblog on their work; and, since I'm not entirely unfamiliar with the concept, I thought I might do that as well. And this blog, being created for me to do Serious Technical Blogging (and then left to gather dust when I stopped being bothered with writing for it), and hosted by Google no less, seems like the best place.
Well. I briefly considered “blogging” by hand-writing an RSS file and giving out that URL — why, some web browsers even format RSS nicely when you browse to it — but then came to my senses. I also considered making a separate blog (as BlogSpot has a nice interface/ontology for that), but didn't really see the point. And, hey, tags; they're what Web 2.0 is all about, except when it's not, or something.
2009-05-21
2008-06-19
Vocabulary Time!
ajax, v.t.: Of a dynamic website, to cause a user to take an unintended action (esp. one difficult or impossible to undo) because the interface rearranged itself (e.g., by removing an item from a list) in delayed response to an earlier action, concurrently with the user's attempting to activate an interface element. Often used passively, as e.g. I just got ajaxed!
2008-06-04
Before It Was Popular?
I remember when I heard about DieHard, the probabilistic memory-safety contrivance, at a talk at NEPLS; that was in 2005, so their PLDI paper wouldn't have existed yet.
And then today I see them get name-checked on hack-a-day — perhaps because they've taken to promoting it as a way to increase the security of the popular web browser Firefox.
Go figure.
And then today I see them get name-checked on hack-a-day — perhaps because they've taken to promoting it as a way to increase the security of the popular web browser Firefox.
Go figure.
2008-04-21
Damn you, Microsoft!
Many people have reason to curse Microsoft, of course, but this is a bit different.
Microsoft's greatest and perhaps only contribution to humanity, the Trackball Explorer, seems to have become a collector's item (with second-hand prices to match!) while I wasn't looking.
Mine is still working (for now), but I'd wanted to have one at home and one at school (read “in the office”), like I did at my last job, which is where I became acquainted with this device, and now that can't happen.
If only I'd known or even suspected back in 2005 or so; I would have picked up a few more.
But perhaps it's only appropriate, given that my extinct trackball is paired with an IBM Model M keyboard which marked its 21st birthday last Thursday. (It was not celebrated, as I'd misremembered the date. Oops.) This means it can legally drink alcoholic beverages now.
Microsoft's greatest and perhaps only contribution to humanity, the Trackball Explorer, seems to have become a collector's item (with second-hand prices to match!) while I wasn't looking.
Mine is still working (for now), but I'd wanted to have one at home and one at school (read “in the office”), like I did at my last job, which is where I became acquainted with this device, and now that can't happen.
If only I'd known or even suspected back in 2005 or so; I would have picked up a few more.
But perhaps it's only appropriate, given that my extinct trackball is paired with an IBM Model M keyboard which marked its 21st birthday last Thursday. (It was not celebrated, as I'd misremembered the date. Oops.) This means it can legally drink alcoholic beverages now.
2008-04-10
Negativity
On Tuesday, I stayed home sick with a cold-and/or-flu (thus missing a class that might have held some information I hadn't yet gotten from the original paper); but people on the Internet were arguing about religion. As they often do. And, as they often do, someone said “it’s true technically you can’t prove a negative”.
This is, of course, false. Negatives can be proven, even without the law of the excluded middle, and even without your logic having a primitive concept of “not”. In, say, the Calculus of Inductive Constructions, “not P” is “P → False”, where “False” is an inductive predicate with no constructors, so you get your ex falso quodlibet just from case analysis, and it's all terribly pretty.
Anyway. Negatives. Even without this newfangled lambda-cube stuff, you can prove that the square root of 2 is irrational, which is to say that there do not exist integers p and q, where q ≠ 0, such that p2 = 2 q2. This was first done around 500 BC, and the person responsible was drowned. Modern Internet religion arguments are, thankfully(?), much tamer.
So, last year, when I was first learning about the Coq proof assistant, I used it to obtain a machine-checkable proof of just that negative. Knowledgeable readers will notice that I independently reinvented part of the NArith library there, because I didn't know about the original.
Thus, what better to do on such a Tuesday, while feverish and generally out of it, but fiddle with an esoteric logic? Which is why I now have a much shorter proof, though I didn't bother mapping it back to the Peano numbers like I did with the other one.
The next obvious thing is, of course, to prove irrational the square roots of other numbers than 2. Or all of them! Or at least all the primes, because it's only in prime bases that the count of trailing zeroes (ctz ≈ bsf) interacts with multiplication in the way needed. (Hints: 2*5=10, 9*9=81.) And that I eventually gave up on.
But, first, I defined subtraction using specification types: given natural numbers a and b, return either c and a proof that a = b + c, or a proof that a < b. And then division: given n and d and a proof of d > 0, return either q and a proof that n = d * q, or a proof that no such q exists.
That last one sounds trivial, but of course it isn't; there's no excluded middle, but, perhaps more to the point, the proof of that “it is or it isn't” can be converted into an actual, runnable, proven-correct OCaml program which does the division. Not that that's very practically useful — it works on Peano numbers and does repeated subtraction (which in turn is repeated decrement).
But it does mark the first time I've successfully used Coq's support for strong induction. Twice, for the division and then for the count-trailing-zeroes, which... or, maybe instead of trying to gloss it into English, I'll just post the original type:
This is, of course, false. Negatives can be proven, even without the law of the excluded middle, and even without your logic having a primitive concept of “not”. In, say, the Calculus of Inductive Constructions, “not P” is “P → False”, where “False” is an inductive predicate with no constructors, so you get your ex falso quodlibet just from case analysis, and it's all terribly pretty.
Anyway. Negatives. Even without this newfangled lambda-cube stuff, you can prove that the square root of 2 is irrational, which is to say that there do not exist integers p and q, where q ≠ 0, such that p2 = 2 q2. This was first done around 500 BC, and the person responsible was drowned. Modern Internet religion arguments are, thankfully(?), much tamer.
So, last year, when I was first learning about the Coq proof assistant, I used it to obtain a machine-checkable proof of just that negative. Knowledgeable readers will notice that I independently reinvented part of the NArith library there, because I didn't know about the original.
Thus, what better to do on such a Tuesday, while feverish and generally out of it, but fiddle with an esoteric logic? Which is why I now have a much shorter proof, though I didn't bother mapping it back to the Peano numbers like I did with the other one.
The next obvious thing is, of course, to prove irrational the square roots of other numbers than 2. Or all of them! Or at least all the primes, because it's only in prime bases that the count of trailing zeroes (ctz ≈ bsf) interacts with multiplication in the way needed. (Hints: 2*5=10, 9*9=81.) And that I eventually gave up on.
But, first, I defined subtraction using specification types: given natural numbers a and b, return either c and a proof that a = b + c, or a proof that a < b. And then division: given n and d and a proof of d > 0, return either q and a proof that n = d * q, or a proof that no such q exists.
That last one sounds trivial, but of course it isn't; there's no excluded middle, but, perhaps more to the point, the proof of that “it is or it isn't” can be converted into an actual, runnable, proven-correct OCaml program which does the division. Not that that's very practically useful — it works on Peano numbers and does repeated subtraction (which in turn is repeated decrement).
But it does mark the first time I've successfully used Coq's support for strong induction. Twice, for the division and then for the count-trailing-zeroes, which... or, maybe instead of trying to gloss it into English, I'll just post the original type:
Definition ctz_spec : forall n b, 1 < b -> { e |
(exists2 m, 0 < m & n = expt b e * m) &
(forall e' m, e < e' -> 0 < m -> n <> expt b e' * m) } + { n = 0 }.
The Spammers Have Won
My last post here warned, in a cryptic and laconic way, of the dangers of trusting automated processes over human judgment — to wit, it was a Google search for the result of people doing a search-and-replace on the font name “Arial” to replace it with the font name “Verdana”, but also altering content as well as markup, and partial words as well as whole. Thus, “adversarial” → “adversverdana”. Cute, huh? (No, I don't go trolling for that kind of thing. I was reading one of the documents so afflicted.)
Apparently, between that and the way that I'll leave this thing unattended for months while meaning to post stuff but not actually doing that thing (in part because, well, originally I'd been hoping to write actual halfway-decent posts here, not twitters-out-of-place like that), I've been declared a possible spam blog and must now transcribe letters from an image to prove my humanity in order to make or edit posts.
Really? In my last job, I got paged in the middle of the night, on weekends, on weekends in the middle of the night, and even on vacation HOW many times, because some mail system had fallen over with its legs in the air from too much spam? And I spent HOW much time delicately tuning Postfix's rate-limiting, because there just wasn't enough hardware for the spam, but I didn't want to delay actual people's LKML subscriptions or whatever as collateral damage? To get this.
So, on the one hand, I can understand where the Google Overlords are coming from, but on the other hand, I'm kind of insulted. And I usually don't take computers' opinions of me all that personally.
Meanwhile, I note that, mysterious spam flag or no, infrequently updated or no, this blog still comes up in the first page of a Google search for... my name. Which, as it's shared by someone famous enough to have his own Wikipedia page, is not a completely vacuous achievement. Or something.
Apparently, between that and the way that I'll leave this thing unattended for months while meaning to post stuff but not actually doing that thing (in part because, well, originally I'd been hoping to write actual halfway-decent posts here, not twitters-out-of-place like that), I've been declared a possible spam blog and must now transcribe letters from an image to prove my humanity in order to make or edit posts.
Really? In my last job, I got paged in the middle of the night, on weekends, on weekends in the middle of the night, and even on vacation HOW many times, because some mail system had fallen over with its legs in the air from too much spam? And I spent HOW much time delicately tuning Postfix's rate-limiting, because there just wasn't enough hardware for the spam, but I didn't want to delay actual people's LKML subscriptions or whatever as collateral damage? To get this.
So, on the one hand, I can understand where the Google Overlords are coming from, but on the other hand, I'm kind of insulted. And I usually don't take computers' opinions of me all that personally.
Meanwhile, I note that, mysterious spam flag or no, infrequently updated or no, this blog still comes up in the first page of a Google search for... my name. Which, as it's shared by someone famous enough to have his own Wikipedia page, is not a completely vacuous achievement. Or something.
2008-04-01
Subscribe to:
Posts (Atom)
