An example why verified programming is hard.
Walking back from where I parked my car today, I realized how difficult it is to make sure specifications are satisfied, once you start looking at them formally. There are specifications with obvious meanings, and obvious algorithms to satisfy them. But ...
After passing the hospital front door, I decided to park in the first available space. The obvious way to do this is to keep driving until I see an available space, and then park in it. But, when I'm finally parking in that space, is it the first available space? Can I know that? When I walked back to the hospital, I saw another available space. It hadn't been available when I drove past it. Was it there when I entered my parking space? I have no idea.
Now this is everyday trivia. But if something like this were to happen in a computer program, and other formal reasoning depended on getting into the first available space, things might get difficult. Would I have to make the specifications weaker? Would I have to make it precise in a complicated way? Would I have to change other code that depended on the details of the spec I could not implement?
Formal verification is hard. Informal verification is impossible. We resort to debugging, and our systems are are vulnerable to attack.
After passing the hospital front door, I decided to park in the first available space. The obvious way to do this is to keep driving until I see an available space, and then park in it. But, when I'm finally parking in that space, is it the first available space? Can I know that? When I walked back to the hospital, I saw another available space. It hadn't been available when I drove past it. Was it there when I entered my parking space? I have no idea.
Now this is everyday trivia. But if something like this were to happen in a computer program, and other formal reasoning depended on getting into the first available space, things might get difficult. Would I have to make the specifications weaker? Would I have to make it precise in a complicated way? Would I have to change other code that depended on the details of the spec I could not implement?
Formal verification is hard. Informal verification is impossible. We resort to debugging, and our systems are are vulnerable to attack.
quantum mechanics and topos theory
I can't say I understand very much of it, but The Physical Interpretation of Daseinisation seems to present a formulation of quantum mechanics in which there's a true state space for quantum systems, which provides actual states for the system to actually be in, independent of any measurements we might want to perform on them. It then identifies classical perspectives on this state space, which represent various ways they might be measured. It turns out that this new formulation gives us an ordinary constructive logic instead of the rather intractible quantum logics theoreticians have been struggling with so far. The nice thing about constructive logics is that it's actually possible to do deductions in them, which seems not to be possible in the so-called quantum logics.
For those up to some heavy mathematics, it's neat stuff.
-- hendrik
For those up to some heavy mathematics, it's neat stuff.
-- hendrik
Project Xanadu
I've just encountered project Xanadu, which seems to have been the original attempt at a true hypertext system -- or at least, one of the early, visionary ones. It seems still to be alive, and its web site and its Australian affiliate have some interesting ideas and critiques of the present web.
Algol 68 compiler
About 40 years ago I had been writing an Algol 68 compiler. I started it at the University of Alberta. It wasn't finished after I spent about two and a half years on it, and I decided that was enough. I has essentially a complete, functioning front end, and a fairly incomplete draft of a code generator. The whole thing was written in Algol W.
When I moved to the Mathematical Centre in Amsterdam it didn't take long for one of its directors to get wind of the incomplete compiler. He had access to an IBM 370, which was compatible with the machine I had first implemented on, so he prevailed on me to resume work on it. I agreed. I now look at that as a mistake. The facilities available weren't as good as they had been in Alberta (TSO instead of MTS, which meant slow turnaround whether I took the train to Delft every day of stayed in Amsterdam and used a 300 bps phone line.) Over the next few years I got the compiler to the point that it correctly handled about half the test set, but it really wasn't ready for serious use.
Then funding ran out, I left the Netherlands, and after that I had essentially no opportunity to continue work on it. Perhaps I could have reimplemented Algol W and then rewrote the code generator for another machine, but in new jobs I had other responsibilities.
Still, I have spent occasional sleepless nights wondering how I *should* have gone about this project.
The first thought is that I should have *started* with the code generator and the inner run-time system (garbage collection, stack management, and the most primitive I/O). There were lots of people writing front ends for Algol 68 compilers. I might have been able to glue someone else's front end to my back end if I had gone in that direction.
The second thought is that I should have gone to complete machine-independence early, rather than late. Algol W might have been a machine-independent language (or close enough to it), but it had been implemented only on the IBM 360 (and therefore also 370), and it was a much bigger language than I needed.
But the real trick is how could I have best gone about that, given the state of the art back in the early 70's when I started the thing.
I now see there were a number of options.
First start in Algol W, as I had, but implementing a small language, possibly a very small Algol 68 sublanguage, that had just the features necessary for writing a compiler. Then rewrite that compiler in its own language, taking care to produce a suitable intermediate code.
(Moving that to a new machine would involve writing a new code generator from the intermediate code, using whatever tools were available on the target machine. Ideally, the intermediate code would have enough redundancy that it could be interpreted as easily as compiled. Ideally, the intermediate code would be word-size-independent, but even if it weren't, it would still be possible to interpret it.).
The small language would have as data types unions, structs, integers, characters, references, and procedures. Most coercions would have to be explicitly coded. There would be no operator or priority declarations, There would probably be other restrictions like this in the direction of explicitness, including a few extra keywords to simplify parsing in places where the Algol 68 is almost, but not quite, ambiguous.
Full type-checking would still be done.
Making these restrictions would cut out a moderate amount of lexical scanner, vastly simplify the context-free parser, wipe out most of the coercion pass, and leave much of the final code-generator and the run-time garbage-collector intact. And this would probably have cut a year or more off total development time (measured in terms of MTS development time, not TSO development time). The system might very well have been machine-independent within two years. Although it wouldn't have been an Algol 68 compiler, it would have been well on the way, and development could have continued on almost any machine. No long-distance phone calls to Delft's computer would have been needed.
There are quite a few techniques I can know of now that might have further accelerated development if they had been known back then. But none of what I've described above involved any technologies I was unfamiliar way back in the early 70's. I could have made the decisions I've just described way back then, except for one important fact:
Back then I lacked the wisdom to go about it this way. The wisdom to get something usable working as soon as possible as opposed to the complete thing sometime later.
-- hendrik
When I moved to the Mathematical Centre in Amsterdam it didn't take long for one of its directors to get wind of the incomplete compiler. He had access to an IBM 370, which was compatible with the machine I had first implemented on, so he prevailed on me to resume work on it. I agreed. I now look at that as a mistake. The facilities available weren't as good as they had been in Alberta (TSO instead of MTS, which meant slow turnaround whether I took the train to Delft every day of stayed in Amsterdam and used a 300 bps phone line.) Over the next few years I got the compiler to the point that it correctly handled about half the test set, but it really wasn't ready for serious use.
Then funding ran out, I left the Netherlands, and after that I had essentially no opportunity to continue work on it. Perhaps I could have reimplemented Algol W and then rewrote the code generator for another machine, but in new jobs I had other responsibilities.
Still, I have spent occasional sleepless nights wondering how I *should* have gone about this project.
The first thought is that I should have *started* with the code generator and the inner run-time system (garbage collection, stack management, and the most primitive I/O). There were lots of people writing front ends for Algol 68 compilers. I might have been able to glue someone else's front end to my back end if I had gone in that direction.
The second thought is that I should have gone to complete machine-independence early, rather than late. Algol W might have been a machine-independent language (or close enough to it), but it had been implemented only on the IBM 360 (and therefore also 370), and it was a much bigger language than I needed.
But the real trick is how could I have best gone about that, given the state of the art back in the early 70's when I started the thing.
I now see there were a number of options.
First start in Algol W, as I had, but implementing a small language, possibly a very small Algol 68 sublanguage, that had just the features necessary for writing a compiler. Then rewrite that compiler in its own language, taking care to produce a suitable intermediate code.
(Moving that to a new machine would involve writing a new code generator from the intermediate code, using whatever tools were available on the target machine. Ideally, the intermediate code would have enough redundancy that it could be interpreted as easily as compiled. Ideally, the intermediate code would be word-size-independent, but even if it weren't, it would still be possible to interpret it.).
The small language would have as data types unions, structs, integers, characters, references, and procedures. Most coercions would have to be explicitly coded. There would be no operator or priority declarations, There would probably be other restrictions like this in the direction of explicitness, including a few extra keywords to simplify parsing in places where the Algol 68 is almost, but not quite, ambiguous.
Full type-checking would still be done.
Making these restrictions would cut out a moderate amount of lexical scanner, vastly simplify the context-free parser, wipe out most of the coercion pass, and leave much of the final code-generator and the run-time garbage-collector intact. And this would probably have cut a year or more off total development time (measured in terms of MTS development time, not TSO development time). The system might very well have been machine-independent within two years. Although it wouldn't have been an Algol 68 compiler, it would have been well on the way, and development could have continued on almost any machine. No long-distance phone calls to Delft's computer would have been needed.
There are quite a few techniques I can know of now that might have further accelerated development if they had been known back then. But none of what I've described above involved any technologies I was unfamiliar way back in the early 70's. I could have made the decisions I've just described way back then, except for one important fact:
Back then I lacked the wisdom to go about it this way. The wisdom to get something usable working as soon as possible as opposed to the complete thing sometime later.
-- hendrik
cancelled TV
I wonder if the propensity of networks to cancel potentially long-running, coherently plotted series during the first season is inhibiting people from starting to watch them, thereby exacerbating the problem.
Multidimensional time
Multidimensional time
In which the author probably reveals his ignorance about quantum mechanics,
or
A little knowledge is a dangerous thing
So it turns out, in Kaluza-Klein theory, it's quite easy to unify electromagnetics and gravity relativistically. And the math is beautiful. So beautiful as to be quite convincing, except for one detail. The theory needs five-dimensional space-time. Where's the extra dimension? Did it go AWOL on a binge in the local bar? I can't really point to a fourth spatial dimension sitting here in my dining room, and, as one physicist put it, he "can't imagine what a universe with two temporal dimensions would be like."
Not only that, but the string theorists have expanded the number of dimensions to ten, or eleven. Didn't I once hear twenty-four? Not only are string-theoretical calculations impossibly difficult for the current generation of mathematicians, but the string theorists have also got to explain away the extra dimensions.
Now maybe the way out is to figure out how multidimensional time could manifest itself.
When you perform a measurement, you can have multiple outcomes. Quantum mechanics teaches us that the outcome is indeterminate. Each different outcome can create a different future. Each different future would have its own single arrow of time with its own series of future events. And from the point of view of someone who has not yet performed the measurement, all of these arrows of time are possible. How many time dimensions do we need to accomodate all these arrows?
In Feynman diagrams, the arrow of time is irrelevant. You have an initial state, a final state, and the particles perform all possible dances getting from the initial state to the final state. What you get to observe is a kind of superposition, a kind of statistical composite (but with complex probabilities) of all the ways of getting from one to the other. How do you fit all those alternatives into one time dimension? Do we even need to? The mathematics is just as happy figuring the probabilities of the initial state given the final state as the other way around.
Perhaps the extra dimensions of Kaluza-Klein and string theories are temporal, and provide room for all these futures.
Perhaps the limitations to two, or seven, or eight, or twenty-one time dimensions aren't even the real constraint on dimensions, but just the number needed for the mathematics.
Foe example, if we take a two-dimensional curved surface, it's cleanly embeddable (locally, at least) in a three-dimensional Euclidean space, faithfully preserving the intrinsic curvature. There's nothing stopping it from being embedded faithfully in a higher dimensional space, but from the viewpoint of the math, three is all that one can derive from the surface geometry.
And I seem to remember hearing of a theorem that if you start with a three (or was it four) dimensional curved hypersurface, it was locally embeddable in a ten-dimensional space.
Perhaps the restriction of, say, ten dimensions is akin to this -- it may only the number of dimensions that actually make a difference, locally.
Perhaps there are an infinite number of these temporal dimensions (whatever "there are" means in sentences like this). But if that is so, we'd have to consider an infinite number of spatial dimensions, too.
In which the author probably reveals his ignorance about quantum mechanics,
or
A little knowledge is a dangerous thing
So it turns out, in Kaluza-Klein theory, it's quite easy to unify electromagnetics and gravity relativistically. And the math is beautiful. So beautiful as to be quite convincing, except for one detail. The theory needs five-dimensional space-time. Where's the extra dimension? Did it go AWOL on a binge in the local bar? I can't really point to a fourth spatial dimension sitting here in my dining room, and, as one physicist put it, he "can't imagine what a universe with two temporal dimensions would be like."
Not only that, but the string theorists have expanded the number of dimensions to ten, or eleven. Didn't I once hear twenty-four? Not only are string-theoretical calculations impossibly difficult for the current generation of mathematicians, but the string theorists have also got to explain away the extra dimensions.
Now maybe the way out is to figure out how multidimensional time could manifest itself.
When you perform a measurement, you can have multiple outcomes. Quantum mechanics teaches us that the outcome is indeterminate. Each different outcome can create a different future. Each different future would have its own single arrow of time with its own series of future events. And from the point of view of someone who has not yet performed the measurement, all of these arrows of time are possible. How many time dimensions do we need to accomodate all these arrows?
In Feynman diagrams, the arrow of time is irrelevant. You have an initial state, a final state, and the particles perform all possible dances getting from the initial state to the final state. What you get to observe is a kind of superposition, a kind of statistical composite (but with complex probabilities) of all the ways of getting from one to the other. How do you fit all those alternatives into one time dimension? Do we even need to? The mathematics is just as happy figuring the probabilities of the initial state given the final state as the other way around.
Perhaps the extra dimensions of Kaluza-Klein and string theories are temporal, and provide room for all these futures.
Perhaps the limitations to two, or seven, or eight, or twenty-one time dimensions aren't even the real constraint on dimensions, but just the number needed for the mathematics.
Foe example, if we take a two-dimensional curved surface, it's cleanly embeddable (locally, at least) in a three-dimensional Euclidean space, faithfully preserving the intrinsic curvature. There's nothing stopping it from being embedded faithfully in a higher dimensional space, but from the viewpoint of the math, three is all that one can derive from the surface geometry.
And I seem to remember hearing of a theorem that if you start with a three (or was it four) dimensional curved hypersurface, it was locally embeddable in a ten-dimensional space.
Perhaps the restriction of, say, ten dimensions is akin to this -- it may only the number of dimensions that actually make a difference, locally.
Perhaps there are an infinite number of these temporal dimensions (whatever "there are" means in sentences like this). But if that is so, we'd have to consider an infinite number of spatial dimensions, too.
Security and Security Theatre
Bruce Schneier has an interesting essay on security and the ways to achieve it or not:
Beyond Security Theater
-- hendrik
Beyond Security Theater
-- hendrik
Distributed revision of word-processor files
Distributed version control systems are more-or-less incompatible with word processors, at least with the current crop of file formats. A DVCS's main job is merging sets of changes that were made independently, possibly at opposite ends of the Earth. They tend to analyze changes in terms of insertion, deletion, and replacement of lines.
But lines are what's not significant in natural-language text, which flows from one line to another like water in a river. And word-processors usually encode the text into some kind of binary file, where the newline characters the DVCS uses are missing.
And the new XML ODT files, even if you uncompress them, aren't particularly helpful, because all their syntax consists of matching brackets of different kinds.
When Betty edits
a b c d e f g h i j
to
a b <i> c d e f </i> g h i j
and George turns it into
a b c d <b> e f g h </b> i j
instead, the result of merging the two sets of changes gives us
a b <i> c d <b> e f </i< g h </b> i j.
which is syntactically invalid XML, and can therefor no longer be edited in the word processor. The users cannot fix the bad merge.
But there are other data representations which may not have these problems, such as infix operators (perhaps with priorities to make sure paragraphs are inside sections and not vice versa). Merging may not always give the right answer, but it will give results that are syntactically valid and therefore can be edited further.
So I ask: Is there some way of accomplishing the things word processors do entirely with infix operators?
-- hendrik
But lines are what's not significant in natural-language text, which flows from one line to another like water in a river. And word-processors usually encode the text into some kind of binary file, where the newline characters the DVCS uses are missing.
And the new XML ODT files, even if you uncompress them, aren't particularly helpful, because all their syntax consists of matching brackets of different kinds.
When Betty edits
a b c d e f g h i j
to
a b <i> c d e f </i> g h i j
and George turns it into
a b c d <b> e f g h </b> i j
instead, the result of merging the two sets of changes gives us
a b <i> c d <b> e f </i< g h </b> i j.
which is syntactically invalid XML, and can therefor no longer be edited in the word processor. The users cannot fix the bad merge.
But there are other data representations which may not have these problems, such as infix operators (perhaps with priorities to make sure paragraphs are inside sections and not vice versa). Merging may not always give the right answer, but it will give results that are syntactically valid and therefore can be edited further.
So I ask: Is there some way of accomplishing the things word processors do entirely with infix operators?
-- hendrik
Another verse to Suzanne
Going through old junk, I just found something I've been looking for for decades. It's another verse to Suzanne, allegedly sung by Leonard Cohen at a Mariposa Folk Festival long ago and transcribed by someone who was there. It's labeled "3/", so presumably it goes after the second verse and before the usual third verse. For all I know my copy may be the only one in the world ... of course it won't be once I post it here.
-- hendrik
3/
All my friends are fast asleep
In places that are high and deep;
Their bodies torn on crosses
Their visions meant to leap;
And in between their dreams
They hate the company they keep.
Nancy lies in London grass.
And Tom in Marco Polo's pass,
Peter slowly dips his toes
In bathtubs filled with Turkish snows.
Leonard hasn't been the same
Since he wandered from his name,
And Alphie(Robert) always loves to tell
How he became invisible at last.
And you want to travel with them,
And you want to travel blind,
And you think you'll maybe trust them
For they've touched your perfect body
With their minds.
-- hendrik
3/
All my friends are fast asleep
In places that are high and deep;
Their bodies torn on crosses
Their visions meant to leap;
And in between their dreams
They hate the company they keep.
Nancy lies in London grass.
And Tom in Marco Polo's pass,
Peter slowly dips his toes
In bathtubs filled with Turkish snows.
Leonard hasn't been the same
Since he wandered from his name,
And Alphie(Robert) always loves to tell
How he became invisible at last.
And you want to travel with them,
And you want to travel blind,
And you think you'll maybe trust them
For they've touched your perfect body
With their minds.
Melissa auf der Maur at Worldcon
Tonight I got to attend a film -- no, a concert -- no, that's not right either, a presentation of Melissa auf der Maur's new multimedia offering, OOOM, Out Of Our Minds. Not the whole thing, just pieces. I got to see the film, which was first presented at Sundance. During breaks in the film (it seems the Palais de Congress has a hard time playing a DVD or Blu-ray disk without equipment failures) she explained what it was like to collaborate with a film-maker. Then she performed a few of her songs. She had no band with her, so she sang, accompanying herself on bass guitar. She said she had never performed without a band before, but the result was overwhelming. I can imagine that the sound would be fuller. smoother, more rounded with a band, but I can only expect it would lose the single-minded intensity it gained from being a one-woman show.
More of this stuff will apparently be shown in performances on the coming months, and the entire multimedia package (including a comic book) will be released early next year.
I will be awaiting it. I hope some of her truly solo performances will be included, because I would be sorry not to hear them again.
-- hendrik
More of this stuff will apparently be shown in performances on the coming months, and the entire multimedia package (including a comic book) will be released early next year.
I will be awaiting it. I hope some of her truly solo performances will be included, because I would be sorry not to hear them again.
-- hendrik
ls is huge
hendrik@lovesong:~$ ls -l /bin/ls
-rwxr-xr-x 1 root root 92312 2008-04-04 10:22 /bin/ls
hendrik@lovesong:~$
92K.
I remember the day when I could use ls on a 48K PDP-11.
That was total memory, including the OS, code space, static data space, and writable data space. Processes could be swapped, but weren't paged, so that really was all the (virtual or real) RAM it could use.
Today'sls wouldn't even fit on that machine 30 years ago. We had entire C compilers that could run on that machine. And generate code that would fit on it, too.
What has happened to software?
What could ls possibly be doing that takes 92K of code?
Not to mention four shared libraries!
hendrik@lovesong:~$ objdump -x /bin/ls | grep NEEDED
-rwxr-xr-x 1 root root 92312 2008-04-04 10:22 /bin/ls
hendrik@lovesong:~$
92K.
I remember the day when I could use ls on a 48K PDP-11.
That was total memory, including the OS, code space, static data space, and writable data space. Processes could be swapped, but weren't paged, so that really was all the (virtual or real) RAM it could use.
Today's
What has happened to software?
What could ls possibly be doing that takes 92K of code?
Not to mention four shared libraries!
hendrik@lovesong:~$ objdump -x /bin/ls | grep NEEDED
NEEDED librt.so.1 NEEDED libselinux.so.1 NEEDED libacl.so.1 NEEDED libc.so.6hendrik@lovesong:~$
(no subject)
I've just started reading The City & The City by China Miéville. Let me recommend it, based only on the four chapters I've already read.
I was told the not to read any of the reviews, but to read the book first. having read only four chapters so far, I don't think I will be able to give away significant spoilers; I can't reveal what I don't know. Nonetheless, I'll be careful here.
It's a police procedural, in an unusual environment. It's meticulously detailed and believable, and that's one of its real strengths. It's also quite strange, in directions not usually explored in science fiction or fantasy, and that is its other strength. So far, at least. I expect more of the author, based on what I've read so far.
I suspect the underlying concept may well be as impossible to describe without spoiling the book as the one in Cryptozoic. So I won't.
-- hendrik
I was told the not to read any of the reviews, but to read the book first. having read only four chapters so far, I don't think I will be able to give away significant spoilers; I can't reveal what I don't know. Nonetheless, I'll be careful here.
It's a police procedural, in an unusual environment. It's meticulously detailed and believable, and that's one of its real strengths. It's also quite strange, in directions not usually explored in science fiction or fantasy, and that is its other strength. So far, at least. I expect more of the author, based on what I've read so far.
I suspect the underlying concept may well be as impossible to describe without spoiling the book as the one in Cryptozoic. So I won't.
-- hendrik
(no subject)
It looks very much that I'll be going to Readercon. The only thing left is to arrange transportation. I'm leaning toward driving, but am concerned about the possibility of highway hypnosis.
(no subject)
liz_marks mentions a tool to find which of your LJ friends have arrived at dreamwidth under the same names:
http://liz-marcs.dreamwidth.org/348682.html
http://liz-marcs.dreamwidth.org/348682.html
Entry tags:
Writer's Block: Shops Gone By
[Error: unknown template qotd]
Marks & Spencer. I know it's still around in the UK, but it's gone from Canada.
Marks & Spencer. I know it's still around in the UK, but it's gone from Canada.
Entry tags:
Writer's Block: Gone but Not Forgotten
[Error: unknown template qotd]
Crusade, the sequel to Babylon 5.
Crusade, the sequel to Babylon 5.