Thanks to the strong leadership of President Bush, we have a real plan for space, as opposed to mostly circling around Earth currently.
Unfortunately, because it's been announced by President Bush, many people who oppose his other policies (for good reason) will also tend to oppose his space policy, even if they would support it if it were proposed by somebody else.
I'm not quiet sure you understand. With a verifying compiler, the programmer defines what is considered correct. The compiler verifies that the program is correct, according to the definition.
Of course, if the definitions are wrong, all bets are off, but it's still an incredibly useful thing to have.
For another example, think of software test suites. Nowadays, you have a programmer explicitly defines a score of situations and checks to make sure that these situations fit defined requirements. With a verifying compiler the programmer still has to define the requirements, but the computer is also able to mathematically prove that any possible set of inputs and situations will obey the defined requirements.
A verifying compiler is a tool that proves automatically that a program is correct before allowing it to run. Program correctness is defined by placing assertions at strategic points in the program text, particularly at the interfaces between its components. These assertions are simply executable truth-valued expressions that are evaluated when control reaches a specific point in a program. If the assertion evaluates to false, then the program is incorrect; if it evaluates to true, then no error has been detected. If it can be proved that it will always evaluate to true, then the program is correct, with respect to this assertion, for all possible executions. These ideas have a long history. In 1950, Turing first proposed using assertions in reasoning about program correctness; in 1967, Floyd proposed the idea of a verifying compiler; and in 1968, Dijkstra proposed writing the assertions even before writing the program.
Early attempts at constructing a verifying compiler were frustrated by the inherent difficulties of automatic theorem proving. These difficulties have inspired productive research on a number of projects, and with the massive increases in computer power and capacity, considerable progress has been made. A second problem is that meaningful assertions are notoriously difficult to write. This means that work on a verifying compiler must be matched by a systematic attempt to attach assertions to the great body of existing software. The ultimate goal is that all the major interfaces in freely available software should be fully documented by assertions approaching in expressive power a full specification of its intended functionality.
But would the results of these related research projects ever be exploited in the production of software products used throughout the world? That depends on the answers to three further questions. First, will programmers use assertions? The answer is yes, but they will use them for many other purposes besides verification; in particular, they are used to detect errors in program testing. Second, will they ever be used for verification of program correctness? Here, the answer is conditional: it depends on wider and deeper education in the principles and practice of programming, and on integration of verification and analysis tools in the standard software development process. Finally, is there a market demand for the extra assurances of reliability that can be offered by a verifying compiler? We think that the answer is yes: the remaining obstacle to the integration of computers into the life of society is a widespread and well-justified reluctance to trust software.
Your mileage may vary, but I've had my (unaltered) gmail account address on the front page of slashdot and some other highly visible places, and fairly little spam seems to get through.
Indeed. I worded my post rather sloppily. If all else is equal, energy efficiency will tend to be selected for. If all else isn't equal, energy efficiency will have to be balanced against other things.
You have to search around a little, but there are good groups still around. For example, I often read sci.space.policy, sci.space.science, and sci.space.tech. science and tech are both moderated. policy isn't moderated, but there's enough good discussions there and it's usually easy to ignore the trolls.
I think I overheard about the game at a party, so I have no idea what the "official" hand gestures (if any) are. When I play I use the following:
Cat: Fingers 1,2,4,5 are legs, middle finger is head
Tinfoil: Just like paper
Microwave: A sort of box made with one or both hands
Cat & Tinfoil: Cat uses legs to scamper with tinfoil, makes joyful meowing sounds
Tinfoil & Microwave: Tinfoil goes in microwave, microwave shakes, makes zappy noises
Microwave & Cat: Cat goes in microwave, beeping noises, panicked meowing, fingers splat out and make gooey explosion noise
More info in research publications
on
Machine Learns Games
·
· Score: 4, Informative
If you actually want to understand what they did, some research publications put out by the CogVis lab have better information regarding the technical side of things.
It's not like they got a camera, gave it AI, pointed it at a rock-paper-scissors game and commanded it to "learn."
Granted, the parent poster is being silly, but that's actually not too far from what they did. They basically took the system and pointed it towards the people playing the game without telling it explicitly what to expect. From the article:
Chris Needham, another member of the CogVis team, says the system's visual processor analyses the action by separating periods of movement and inactivity and then extracting features based on colour and texture. Combining this with audio input, the system develops hypotheses about the game's rules using an approach known as inductive logic programming.
"It was very impressive," says Max Bramer, a researcher at Portsmouth University, UK, and chair of the British Computer Society's AI group. He told New Scientist that CogVis could have many future applications. "You can think of lots of times when you'd like to be able to point a camera at something and have a computer interpret things for itself."
He suggests that machine's could one day use this technique to learn how to spot an intruder on video footage or how to control a robot for important maintenance work. "It's a very good start, and almost mysterious in the way it works," Bramer adds.
From their page:
In this piece of work we are attempting to learn descriptions of objects and events in an entirely autonomous way. Our aim is zero human interference in the learning process, and only to use non scene specific prior information. The resulting models (object and protocol) are used to drive a synthetic agent that can interact in the real world.
I always preferred "cat, tinfoil, microwave" myself. Cat rips tinfoil, tinfoil zaps microwave, microwave 'splodes cat. The looks on other people's faces when they see you playing it is well worth it.
How does a synapse know whether to remember something or not... answer - it doesn't.
Well, that's not quite true. Some synapses are truely "unsupervised," strengthening when, for example, the two neurons it connects fire at the same time. Other synapses strengthen or weaken when exposed to certain chemicals, like calcium or dopamine.
I personally think that the source of all human illness is basically the body forgetting how to maintain itself... critical synapses failing.
This may be true for certain neurological diseases, but all human illness? I rather doubt that.
I wouldn't be so quick to dismiss it. Terry Sejnowski is probably one of the most prominent neuroscientists alive today, and generally knows what he's talking about.
You do not need constancy of material/molecules to keep a memory - in a sense you can exchange a building brick by brick, one at a time, with new bricks, and maintain your building like new, for millenia.
This is true, and undoubtedly works well for short-term and medium-term memories. However, all of this exchange takes energy, and if there's a more energy efficient way of doing things (such as, perhaps, storing memories in the extracellular matrix), evolution would tend to select in favor of it.
There's actually a Wikipedia-related project called Wikibooks, dedicated to using the wiki process to collaboratively create textbooks. I think the OP's work would be an excellent contribution to this project.
Wow, because mega-corporations make much better decisions than countries about treating employees/citizens!
The point isn't that CEOs make smarter or dumber decisions than politicians. The point is that when they do make dumb decisions, you can choose another option -- you don't have somebody putting a gun to your head if you don't accept the decision.
Yeah, god forbid that companies have a dominant role in spaceflight, like they have in airflight. Just look at all the oppression and inter-company warfare we've seen since companies have started to operate air services (for a fee, even!).
Believe it or not, it's somewhat difficult for a commercial company to compete in an industry where other (much larger and established) companies are getting billions of dollars in cost-plus contracts from the government. That's the main reason you haven't seen plenty of commercial companies in the field.
They were planning on flying last year, but problems with getting the engine working properly prevented that from happening. Hopefully this latest news means those problems have been resolved.
The engine which was tested will be used on both the Falcon I and Falcon V.
Just how is their Merlin engine different from the Russian RD-180?
An individual RD-180 costs $10 million. The price-per launch that Musk is charging for the entire Falcon I is $6 million. Putting a $10 million engine on a rocket that you're charging $6 million for doesn't seem particularly economical.
Renting Baikonur and hiring Russian specialists would have cost him half as much and the results would be much better, IMHO.
Yeah, and make it impossible for him to launch US satellites.
It's interesting to note that the Chinese made cheap, disposable wooden heatshields. It's certainly not the most glamorous thing around, but it gets the job done.
From the link:
The Chinese had developed another novel but usable "low tech" solution. They glued up wooden blocks, appropriately contoured, with the end grain facing the reentry air stream. The wooden heat shield would char and ablate during reentry, just like the caulk material on the Apollo capsules. The fact that you could build a serviceable heat shield for reentry from space out of wood certainly showed that the basic problem was not insurmountably difficult, so Tom had always regarded this too as a rather straight-forward challenge.... Wood can't withstand directly the temperatures of reentry, but for that relatively short time, it can resist those temperatures by gradually eroding.... As the wood heated, a carbon ceramic char formed on the outer surface, and the volatiles, or fluids, in the wood behind the char flowed up through cracks in the char. Heat was radiated away from the charred surface, and the interior was kept cool by the outward movement of the cooler heat-absorbing volatiles flowing towards the hot side.
Someone is putting his money where my mouth has been. Describing permanent settlement of Mars as "a positive, constructive, inspirational goal" capable of uniting humanity at a critical time," dot-com entrepreneur Elon Musk has pledged a substantial portion of his personal fortune to realizing that goal, beginning with a proposed $20 million technology-demonstration Mars lander to be launched perhaps in 2005. Calling his "victory condition" seeing NASA's top priority change to establishing a permanent human presence on Mars, he said in an interview last week that "the path by which I hope to get there is to get the public enthusiastic about the possibility, then translate that into legislative pressure so that Congress hands us a Mars mandate." Musk's plans are invigorating, finally matching for Mars the initiative and boldness recently displayed in Low Earth Orbit by Dennis Tito's flight and the recent MirCorp announcement of a private "MiniMir" orbiting facility. I hope his entrepreneurial directness will bring a new effectiveness to the Mars effort. I hope also that he can avoid being brought down by the Byzantine politics of space: on the Hill, in the scientific community and in the space movement.
NASA wants to know whether there ever was life on Mars. Musk - and I, and many more - want to know if there ever can be.
Musk's "Mars Oasis" project is a small robotic lander intended primarily as a mini-greenhouse, growing samples of food crops in an enclosed chamber filled with treated Martian regolith (soil), to test the feasibility of humans living off the land. Other experiments may include test units for the production of oxygen and rocket fuel from the Martian atmosphere, and radiation sensors. In a radical departure from the missions scheduled by NASA, each experiment would focus on developing data critical to human habitation, rather than on pure planetary science. While the project's centerpiece is essentially the project long advocated by NASA planetary scientist Chris McKay, Musk stated that he had only met McKay in passing and had not discussed the project with him....
His goal of moving Congress to declare a human presence on Mars to be a priority implies substantial legislative action, at the very least putting forward a legislative program to be advocated to Congress by citizen supporters.
I think he's actually spending a pretty modest amount on development. From an older interview:
While Musk said he is not the company's sole backer, he said he is prepared to fund the development of the Falcon LV entirely out of his own pocket if he has to. He declined to say exactly how much he expects to spend developing the rocket, only that the figure will be "in the tens of millions" of dollars.
Slashdot Mirror
Thanks to the strong leadership of President Bush, we have a real plan for space, as opposed to mostly circling around Earth currently.
Unfortunately, because it's been announced by President Bush, many people who oppose his other policies (for good reason) will also tend to oppose his space policy, even if they would support it if it were proposed by somebody else.
There's a apparently a babelfish plugin for gaim, and gaim supports IRC, so...
s/quiet/quite
I'm not quiet sure you understand. With a verifying compiler, the programmer defines what is considered correct. The compiler verifies that the program is correct, according to the definition.
Of course, if the definitions are wrong, all bets are off, but it's still an incredibly useful thing to have.
For another example, think of software test suites. Nowadays, you have a programmer explicitly defines a score of situations and checks to make sure that these situations fit defined requirements. With a verifying compiler the programmer still has to define the requirements, but the computer is also able to mathematically prove that any possible set of inputs and situations will obey the defined requirements.
From the BCS report:
A verifying compiler is a tool that proves automatically that a program is correct before allowing it to run. Program correctness is defined by placing assertions at strategic points in the program text, particularly at the interfaces between its components. These assertions are simply executable truth-valued expressions that are evaluated when control reaches a specific point in a program. If the assertion evaluates to false, then the program is incorrect; if it evaluates to true, then no error has been detected. If it can be proved that it will always evaluate to true, then the program is correct, with respect to this assertion, for all possible executions. These ideas have a long history. In 1950, Turing first proposed using assertions in reasoning about program correctness; in 1967, Floyd proposed the idea of a verifying compiler; and in 1968, Dijkstra proposed writing the assertions even before writing the program.
Early attempts at constructing a verifying compiler were frustrated by the inherent difficulties of automatic theorem proving. These difficulties have inspired productive research on a number of projects, and with the massive increases in computer power and capacity, considerable progress has been made. A second problem is that meaningful assertions are notoriously difficult to write. This means that work on a verifying compiler must be matched by a systematic attempt to attach assertions to the great body of existing software. The ultimate goal is that all the major interfaces in freely available software should be fully documented by assertions approaching in expressive power a full specification of its intended functionality.
But would the results of these related research projects ever be exploited in the production of software products used throughout the world? That depends on the answers to three further questions. First, will programmers use assertions? The answer is yes, but they will use them for many other purposes besides verification; in particular, they are used to detect errors in program testing. Second, will they ever be used for verification of program correctness? Here, the answer is conditional: it depends on wider and deeper education in the principles and practice of programming, and on integration of verification and analysis tools in the standard software development process. Finally, is there a market demand for the extra assurances of reliability that can be offered by a verifying compiler? We think that the answer is yes: the remaining obstacle to the integration of computers into the life of society is a widespread and well-justified reluctance to trust software.
Your mileage may vary, but I've had my (unaltered) gmail account address on the front page of slashdot and some other highly visible places, and fairly little spam seems to get through.
Indeed. I worded my post rather sloppily. If all else is equal, energy efficiency will tend to be selected for. If all else isn't equal, energy efficiency will have to be balanced against other things.
You have to search around a little, but there are good groups still around. For example, I often read sci.space.policy, sci.space.science, and sci.space.tech. science and tech are both moderated. policy isn't moderated, but there's enough good discussions there and it's usually easy to ignore the trolls.
I think I overheard about the game at a party, so I have no idea what the "official" hand gestures (if any) are. When I play I use the following:
Cat: Fingers 1,2,4,5 are legs, middle finger is head
Tinfoil: Just like paper
Microwave: A sort of box made with one or both hands
Cat & Tinfoil: Cat uses legs to scamper with tinfoil, makes joyful meowing sounds
Tinfoil & Microwave: Tinfoil goes in microwave, microwave shakes, makes zappy noises
Microwave & Cat: Cat goes in microwave, beeping noises, panicked meowing, fingers splat out and make gooey explosion noise
If you actually want to understand what they did, some research publications put out by the CogVis lab have better information regarding the technical side of things.
Towards an Architecture for Cognitive Vision Using Qualitative Spatio-temporal Representations and Abduction (Cohn et al, 2003)
Modeling interaction using learnt qualitative spatio-temporal relations and variable length Markov models (Galata et al, 2002)
(On that note, I think it will be the one sure sign of true artificial intelligence when our programs start 'cheating' to win.)
The impression I get from reading through their work is that if the program observed a human cheating, it could potentially learn how to imitate it.
It's not like they got a camera, gave it AI, pointed it at a rock-paper-scissors game and commanded it to "learn."
Granted, the parent poster is being silly, but that's actually not too far from what they did. They basically took the system and pointed it towards the people playing the game without telling it explicitly what to expect. From the article:
Chris Needham, another member of the CogVis team, says the system's visual processor analyses the action by separating periods of movement and inactivity and then extracting features based on colour and texture. Combining this with audio input, the system develops hypotheses about the game's rules using an approach known as inductive logic programming.
"It was very impressive," says Max Bramer, a researcher at Portsmouth University, UK, and chair of the British Computer Society's AI group. He told New Scientist that CogVis could have many future applications. "You can think of lots of times when you'd like to be able to point a camera at something and have a computer interpret things for itself."
He suggests that machine's could one day use this technique to learn how to spot an intruder on video footage or how to control a robot for important maintenance work. "It's a very good start, and almost mysterious in the way it works," Bramer adds.
From their page:
In this piece of work we are attempting to learn descriptions of objects and events in an entirely autonomous way. Our aim is zero human interference in the learning process, and only to use non scene specific prior information. The resulting models (object and protocol) are used to drive a synthetic agent that can interact in the real world.
I always preferred "cat, tinfoil, microwave" myself. Cat rips tinfoil, tinfoil zaps microwave, microwave 'splodes cat. The looks on other people's faces when they see you playing it is well worth it.
Seriously though, this is really cool research.
How does a synapse know whether to remember something or not... answer - it doesn't.
Well, that's not quite true. Some synapses are truely "unsupervised," strengthening when, for example, the two neurons it connects fire at the same time. Other synapses strengthen or weaken when exposed to certain chemicals, like calcium or dopamine.
I personally think that the source of all human illness is basically the body forgetting how to maintain itself... critical synapses failing.
This may be true for certain neurological diseases, but all human illness? I rather doubt that.
http://scholar.google.com/scholar?hl=en&lr=&q=creb +memory&btnG=Search
That's bullshit.
I wouldn't be so quick to dismiss it. Terry Sejnowski is probably one of the most prominent neuroscientists alive today, and generally knows what he's talking about.
You do not need constancy of material/molecules to keep a memory - in a sense you can exchange a building brick by brick, one at a time, with new bricks, and maintain your building like new, for millenia.
This is true, and undoubtedly works well for short-term and medium-term memories. However, all of this exchange takes energy, and if there's a more energy efficient way of doing things (such as, perhaps, storing memories in the extracellular matrix), evolution would tend to select in favor of it.
There's actually a Wikipedia-related project called Wikibooks, dedicated to using the wiki process to collaboratively create textbooks. I think the OP's work would be an excellent contribution to this project.
Wow, because mega-corporations make much better decisions than countries about treating employees/citizens!
The point isn't that CEOs make smarter or dumber decisions than politicians. The point is that when they do make dumb decisions, you can choose another option -- you don't have somebody putting a gun to your head if you don't accept the decision.
Yeah, god forbid that companies have a dominant role in spaceflight, like they have in airflight. Just look at all the oppression and inter-company warfare we've seen since companies have started to operate air services (for a fee, even!).
Believe it or not, it's somewhat difficult for a commercial company to compete in an industry where other (much larger and established) companies are getting billions of dollars in cost-plus contracts from the government. That's the main reason you haven't seen plenty of commercial companies in the field.
They were planning on flying last year, but problems with getting the engine working properly prevented that from happening. Hopefully this latest news means those problems have been resolved.
The engine which was tested will be used on both the Falcon I and Falcon V.
Just how is their Merlin engine different from the Russian RD-180?
An individual RD-180 costs $10 million. The price-per launch that Musk is charging for the entire Falcon I is $6 million. Putting a $10 million engine on a rocket that you're charging $6 million for doesn't seem particularly economical.
Renting Baikonur and hiring Russian specialists would have cost him half as much and the results would be much better, IMHO.
Yeah, and make it impossible for him to launch US satellites.
It's interesting to note that the Chinese made cheap, disposable wooden heatshields. It's certainly not the most glamorous thing around, but it gets the job done.
... Wood can't withstand directly the temperatures of reentry, but for that relatively short time, it can resist those temperatures by gradually eroding. ... As the wood heated, a carbon ceramic char formed on the outer surface, and the volatiles, or fluids, in the wood behind the char flowed up through cracks in the char. Heat was radiated away from the charred surface, and the interior was kept cool by the outward movement of the cooler heat-absorbing volatiles flowing towards the hot side.
From the link:
The Chinese had developed another novel but usable "low tech" solution. They glued up wooden blocks, appropriately contoured, with the end grain facing the reentry air stream. The wooden heat shield would char and ablate during reentry, just like the caulk material on the Apollo capsules. The fact that you could build a serviceable heat shield for reentry from space out of wood certainly showed that the basic problem was not insurmountably difficult, so Tom had always regarded this too as a rather straight-forward challenge.
If anyone's curious, here's a little more info on his old "Life to Mars" project:
...
MarsNow 1.9 Profile: Elon Musk, Life to Mars Foundation
Someone is putting his money where my mouth has been. Describing permanent settlement of Mars as "a positive, constructive, inspirational goal" capable of uniting humanity at a critical time," dot-com entrepreneur Elon Musk has pledged a substantial portion of his personal fortune to realizing that goal, beginning with a proposed $20 million technology-demonstration Mars lander to be launched perhaps in 2005. Calling his "victory condition" seeing NASA's top priority change to establishing a permanent human presence on Mars, he said in an interview last week that "the path by which I hope to get there is to get the public enthusiastic about the possibility, then translate that into legislative pressure so that Congress hands us a Mars mandate." Musk's plans are invigorating, finally matching for Mars the initiative and boldness recently displayed in Low Earth Orbit by Dennis Tito's flight and the recent MirCorp announcement of a private "MiniMir" orbiting facility. I hope his entrepreneurial directness will bring a new effectiveness to the Mars effort. I hope also that he can avoid being brought down by the Byzantine politics of space: on the Hill, in the scientific community and in the space movement.
NASA wants to know whether there ever was life on Mars. Musk - and I, and many more - want to know if there ever can be.
Musk's "Mars Oasis" project is a small robotic lander intended primarily as a mini-greenhouse, growing samples of food crops in an enclosed chamber filled with treated Martian regolith (soil), to test the feasibility of humans living off the land. Other experiments may include test units for the production of oxygen and rocket fuel from the Martian atmosphere, and radiation sensors. In a radical departure from the missions scheduled by NASA, each experiment would focus on developing data critical to human habitation, rather than on pure planetary science. While the project's centerpiece is essentially the project long advocated by NASA planetary scientist Chris McKay, Musk stated that he had only met McKay in passing and had not discussed the project with him.
His goal of moving Congress to declare a human presence on Mars to be a priority implies substantial legislative action, at the very least putting forward a legislative program to be advocated to Congress by citizen supporters.
I think he's actually spending a pretty modest amount on development. From an older interview:
While Musk said he is not the company's sole backer, he said he is prepared to fund the development of the Falcon LV entirely out of his own pocket if he has to. He declined to say exactly how much he expects to spend developing the rocket, only that the figure will be "in the tens of millions" of dollars.