Want to read Slashdot from your mobile device? Point it at m.slashdot.org and keep reading!


Forgot your password?
DEAL: For $25 - Add A Second Phone Number To Your Smartphone for life! Use promo code SLASHDOT25. Also, Slashdot's Facebook page has a chat bot now. Message it for stories and more. Check out the new SourceForge HTML5 Internet speed test! ×

Comment Re:Good News and Bad News (Score 1) 517

First off, as an Australian and a nerd, I am very proud.


Good news: there is now a formally verified microkernel. 8,700 lines of C and 600 odd lines of ARM assembly. Awesome.

Bad news: it took 200,000 lines of manually-generated proof and approximately 25 person-years by PhDs to verify the aforementioned microkernel.

Conclusion: formal verification of software is not going to take off any time soon.

25 man-years is not that much, if we really valued it. If the process is modular, 100 persons do 25 man-years in 3 months. Now, I have no idea by what method this was performed, but surely it has to at least be modular over different programs, so that we could, if we really cared about it, have a formally proven whole distribution in a few years.

It is by no means out of reach.

But you are right that it would take all the required man-years away from developing time, so we can be quite confident that it will not be adopted, it would slow down developing time too much to justify the cost for most developers.

Comment Re:What's this new obsession with the Chinese... (Score 1) 439

The US military seems to think otherwise. Here a quote from an article in The Economist about the militarisation of space (http://www.economist.com/science/displaystory.cfm?story_id=10533205). The numer of nulcear missiles is not the only thing determining the outcome of a military conflict...

But the Pentagon worries about what would happen if America came up against a major power, a "near-peer" rival (as it calls China and Russia), able to intercept space assets with missiles and "space mines", or to disable them with lasers and electronic jammers. "There are a lot of vulnerabilities," admits an American general, "There are backups, but our space architecture is very fragile."

The precise nature of these weaknesses is a well-guarded secret. But wargames simulating a future conflict over Taiwan often end up with the "Red Force" (China) either defeating the "Blue Force" (America) or inflicting grievous losses on it by launching an early attack in space, perhaps by setting off one or more nuclear explosions above the atmosphere. "I have played Red and had a wonderful time," says the general, "It is pretty easy to disrupt Blue. We should not expect an enemy to play by established norms in space. They will play dirty pool."

Slashdot Top Deals

Yes, we will be going to OSI, Mars, and Pluto, but not necessarily in that order. -- Jeffrey Honig