That's not really a big improvement. General Electric's big wind turbines (1.5 to 3.5 megawatts) cut in at 3.5 m/sec. Vesta large wind turbines cut in at 4 m/sec. At the low end of the size range, the classic Jacobs wind turbines cut in at 8 mph. Magnetic bearings aren't that exotic; they look like electric motors. Bearing losses aren't that big anyway, although wind turbines do have tough bearing requirements. So it's not clear that magnetic bearings are worth the trouble.
The big breakthrough in wind has been in energy conversion. The older large wind turbines were AC syncronous machines, and had to sync to the power grid. That's why, when you see older wind farms like Pacheco Pass, all the blades are turning in sync. Modern units free-run, and there's an AC to DC to AC conversion with rectifiers and inverters to convert the output to 60Hz. This lowers the cut-in speed; with older systems, you couldn't get any power out until there was enough wind to get the generator up to 60Hz speed.
Software sucks because the costs of it sucking fall on the user, not the manufacturer. That's hasn't been true of automobiles for several decades now, and cars have gotten much better. When was the last time your car died on the road?
Many years ago, I was at Ford Aerospace when the Ford EEC-IV electronic engine control unit was being developed. In that unit, the program was permanent; it was in a mask-programmed device, and could not be changed without replacing the entire unit. Very substantial resources were devoted to insuring that there were no bugs that could cause cars to fail on the road. There was huge fear of a recall; if something had gone wrong, most of the
Ford cars on the road would have to come back to a dealership for CPU replacement. There were old engineers at Ford who didn't want a computer to have direct control of the engine. Tweak the spark timing a bit or adjust the emissions valves, like the earlier models of engine control, perhaps. But actually fire the spark plug directly from software? That was radical. So everyone involved was paranoid about bugs.
It worked. Twenty years later, no bugs have been found. There was never an EEC-IV recall. The EEC-IV is still popular with enthusiasts. You can even download the code and run it in an emulator. I still have a 1985 Ford Bronco with its original EEC-IV, and it runs fine.
If Microsoft had to face the possibility of bringing every PC with Windows on it into an approved Microsoft repair center for a software update at Microsoft's expense, Windows would not crash. It might not do as much, but critical components of it wouldn't fail disasterously.
There are several pro-Israel monitoring services watching the press - CAMERA in the US, BICOM in the UK, and MEMRI to monitor the Arab press. CAMERA is noted for having a good database of stories about Israel. Apparently stories mentioning Israel are found automatically, but evaluated by people.
The CIA has something called the "Open Source Intelligence Service", which started as the "Foreign Broadcast Monitoring Service". Visualize some poor guy spending eight hours a day listening to Radio Albania, all through the Cold War. Most of the content is terminally boring, but then, one day the announcer says "so we're invading Yugoslavia", and the CIA needs to notice this. There have been repeated attempts to automate the job.
Wind turbines are only useful if the average wind speed is above 10 mph. The unit illustrated doesn't even cut in until 8 mph, and achieves its rated output at a wind speed of 20 mph.
Unless you're in an area with wind speeds like that, a wind turbine is a waste of time. Most people don't live in areas that windy; it's not comfortable. I've known people along the California coast who have useful wind turbines, but that's a special situation, where you have reliable medium-speed wind all year because of the ocean/land temperature difference. The serious California wind farms are in mountain passes or at desert/mountain boundaries, where the geography guarantees wind. Also, wind speeds are higher a few hundred feet up, which is why the really big wind machines on the high towers work even in flat terrain. A little turbine in your back yard probably is just going to sit there, stationary, most of the time.
If you're thinking of getting a wind turbine, put up a pole with one of those little "weather station" units that has an anemometer, and log wind speeds for a year. For a few hundred dollars, you'll find out if it's going to work.
If you can hang a wind chime outside your house and it doesn't drive you nuts with constant clanging, your location is not suitable for wind power.
They made it "fanless", right? Fanless electronic devices with significant heat loads are inherently vulnerable; if the external environment is worse than the design spec, they die. Hot weather or tight shelf space, and you're dead.
Worse, if some systems are failing early in life due to cooling problems, more are very likely to fail later. ICs that run hot has a reduced lifespan; there's a well-understood relationship for this. So if demo units are failing when new, this is serious.
Somewhere at Sony, I suspect that engineers are frantically trying to tweak the heatsink, airflow, and case hole design before shipping. It's very late for that.
There will probably be aftermarket fan kits. Liquid cooling would be overdoing it.
That review reads like one of those suck-up reviews from a game mag supported by game advertising. Is this game advertised on Slashdot?
From the description, the game sounds like what, in the industry, is derisively called a "track ride", where you're led by the nose through a canned story.
Re:First things first
on
Caller ID Watches
·
· Score: 2, Informative
I'm wearing one. It's a Casio watch which receives WWV. It sets itself every night at 2 AM. Knows the date. Adjusts for daylight savings time. Solar-powered, so it doesn't need battery replacement. So it doesn't need any attention. Lights up if you rotate your wrist rapidly. Waterproof and rugged enough to survive outdoor activities. Costs about $50.
This definitively solves the "what time is it" problem for locations in the United States. Anything beyond this is bling.
DARPA has been funding this kind of thing for years. Small turbines have resulted. DARPA was originally trying to develop bird-sized unmanned aerial vehicles. That R&D program produced some flyable devices, but they didn't have the low cost and 2-hour endurance DARPA wanted.
DARPA-funded work at MIT resulted in some microturbine parts back in 1997. Progress has been slower than expected, but it's happening.
The microgenerator thing was intended as a military application. The idea is to have something small, maybe even wearable, a soldier can use to recharge all the battery-operated gear. Battery recharging in the field, where power outlets are rare, is getting to be a huge hassle in the US military. Current technology is to put power outlets on everything with wheels and an engine, but that creates its own headaches.
But beyond the punditry, the big problem is that the US is losing manufacturing jobs. Most productivity growth is in manufacturing; productivity in services increases very slowly. Janitors and sales reps are barely more productive than they were decades ago.
The US is losing in high-tech products, too. For decades, the US exported far more high-tech products than it imported. That ended in 2002. Since then, imports have exceeded exports. And that's in high-tech; it's far, far worse in steel, textiles, general manufactured goods...
What's striking is how fast this has happened. There's been a huge change in the US economy since 2000. It's not a recession; it's a fundamental loss of productive capacity. Entire industries have disappeared in the US; textiles, paper, machine tools... computers. Very few computers are actually made in the US.
This is finally getting attention because upper management is being "outsourced". First the manufacturing moves offshore. Then the engineering. Then the marketing operation becomes a small unit in Bentonville to interface with WalMart. Financing starts to come from Hong Kong and Dubai instead of New York.
At that point, there's no reason for expensive upper management in the US.
The IBM PC saga is instructive. It's Lenovo now. Principal operations are in Beijing. There's an "executive headquarters" in Raleigh, NC. They're hiring; they have about 250 openings. One is high-level technical (wireless networking interoperability). Five are low-level technical. The others are all sales-related, except for some people in "accounts receivable" doing collections.
Lenovo started out with more ex-IBM execs, but they're gradually disappearing.
Warren Slocum, who is in charge of elections here in San Mateo county, is extremely critical of touch-screen voting machines. He liked the system we had here - big paper ballots marked with black markers, which the voter inserts into the scanner atop the ballot box. This gives a quick count when the polls close, and the ballots are locked in the box in case a recount is needed.
But we couldn't keep that system. It wasn't compliant with the "Help America Vote Act", which requires touch-screen machines for "accessability" by blind people. San Mateo had to go touch-screen, but it went with Hart InterCivic eSlate machines. They're still not high-security devices, but they're way better than the Diebold crap. Slocum pushed to get California to require printers for manual recounts on all California touch-screen machines, and that's now the law in California.
But Hart InterCivic has problems, too.
"Gail Fisher, manager of the county's Elections Division (for Travis, TX), theorizes that after selecting their straight
party vote, some voters are going to the next page on the electronic ballot and pressing "enter,"
perhaps thinking they are pressing "cast ballot" or "next page." Since the Bush/ Cheney ticket is the
first thing on the page, it is highlighted when the page comes up - and thus, pressing "enter" at that
moment causes the Kerry/ Edwards vote to be changed to Bush/ Cheney."
What CMU is selling (and yes, they're operating a business) is like those remote-controlled "entertainment robots" of the 1980s. There's apparently someone in the background running the thing. Big deal.
Now here's a useful entertainment robot - the MotoMan RoboBar This is a two-armed industrial robot bartender. For real.
The MotoMan RoboBar is from the leading robotics company from Japan, Yaskawa Electric. Over 120,000 robots installed. Their slogan is intimidating: "We already make your car. Let us make your drink". While CMU is making toys, Yaskawa is automating the world.
It's even worse. Look at the examples in the article. The upconverted versions have big rectangular compression artifacts. So not only were they upconverted, they were decompressed and recompressed, which generates terrible artifacts. (See most files on YouTube for examples.) If they'd just been upconverted from low-rez source material, they'd just be blurry.
MAYBE NONE OF, PROBABLY ALL OF, AND DEFINITELY MORE THAN:
New ways of getting your load onto your quivering victim's stack
Reaching into the hearts and minds (also the genitals) of users.
Firefox re-entrant threading lols
Patching BIOS for kernel-patching rootkit memory injections
Aggresive AIM attacks and escapades
Internet hilarity, sexual innuendo, LOLDONGS
Well, I'll say one thing for them. They put enough bandwidth behind the site that the video downloaded without any delays. Go ahead, watch the Quicktime version.
Here's the SCO vs IBM case schedule. Note how many key steps are now complete and in the past. Discovery is over. Expert reports are over. The final deadline for expert discovery passed last week. No more surprises. No more "secret evidence". No more stalling. We're past that. All the evidence is on the table now. The process grinds slowly, but it does grind.
Now the process speeds up. There's a significant deadline every few weeks now. Right now, summary judgement motions are being briefed and decided. That may end the case in favor of IBM, and it will almost certainly narrow it, as SCO's unsupported claims are knocked down. Those will be decided by the end of the year.
In January, the pace speeds up even more. As trial approaches, there are judge-set deadlines every few days.
If there's anything left to try, trial starts February 26, 2007. Not that far away.
The Internet Archive has an ongoing effort to measure disk drive reliability. They have several thousand disk drives for which they are collecting data, and for the year 2005, about 2% failed. This is better than previous years; a few years back they were experiencing 6%/year failure rates.
They send them back for warranty replacement, I'm told.
What is the semantic difference between C and Pascal?
The big problems with C/C++ from a formal methods standpoint:
void* (You lose all the type information)
Too much casting. (Again, you lose all the type information)
Array size information isn't carried along with arrays or passed through function calls. (Biggest design mistake in C).
The "array is a pointer to the first element" convention. (Is this an array or a single object?)
Pointer arithmetic semantics are ill defined. (Long story.)
C++ iterators don't have an explicit tie to the collection, so detecting iterator invalidation statically is hard.
Hard to detect aliasing. (A consequence of the free use of pointers.)
Too much "undefined behavior" that isn't prohibited.
I would expect pointer arithmetic to be the source of problems, but if I recall correctly, Pascal's pointers have arithmetic as well.
No, they don't.
Pointer arithmetic really is obsolete. Compilers have been generating code for subscripting that's as good or better than pointer arithmetic code for well over a decade now.
The main reason program verification didn't catch on was that it was hopeless for C and C++. The semantics of those languages were so messy that formalizing them was nearly hopeless.
Java and C#, however, are good enough. (So were Pascal, Modula, and Ada.)
Here's the manual for the Pascal-F verifier, a system written by a team I headed back in the early 1980s. This was a proprietary system done internally for Ford Motor Company. Take a look at the example real time engine control program beginning on page 155. It was painfully slow back then; it took 45 minutes of VAX 11/780 time (1 MIPS) to verify that program from a cold start. Today, it would take about a second.
What's being proved in that example? First, that there are no subscripts out of range or arithmetic overflows. Second, that all loops terminate. (Yes, you can prove that for most useful programs; the halting problem applies only to pathological programs.)
Third, that the following constraints hold:
fuelpumpon implies (tickssincespark < (1000*ms)); if fuel pump is on, spark must occur within 1 sec.
(enginespeed < rpm(1)) implies (not fuelpumpon); fuel pump must be disabled if the
engine is not rotating
cylssincespark <= 1; a spark must be issued for each cylinder pulse
Useful stuff, the conditions needed to keep the engine running.
This is "design by contract" with teeth. Each function is checked to insure that it always satisfies its exit conditions if its entry conditions are satisfied by the caller, and that the function doesn't overflow, subscript out of range, or fail to terminate. Each call is checked to insure that its entry conditions are always satisfied. The end result is a guarantee that those properties hold for the whole program.
This is a very valuable check. It insures that caller and callee are in agreement on how to call each function. That's the cause of a huge number of software bugs - the caller made some incorrect assumption about the function being called, or the function didn't check for something which it needed to check. Both of those can be statically machine checked.
It's not easy to get a program through formal verification with a verifier like that one. The verifier does almost all the work on easy sections of code, but where correctness depends on anything non-trivial, you have to work with the theorem prover to get the proofs through. This isn't easy. The DEC Java checker and Microsoft's Spec# checker aren't as hard-line.
Slashdot Mirror
That's not really a big improvement. General Electric's big wind turbines (1.5 to 3.5 megawatts) cut in at 3.5 m/sec. Vesta large wind turbines cut in at 4 m/sec. At the low end of the size range, the classic Jacobs wind turbines cut in at 8 mph. Magnetic bearings aren't that exotic; they look like electric motors. Bearing losses aren't that big anyway, although wind turbines do have tough bearing requirements. So it's not clear that magnetic bearings are worth the trouble.
The big breakthrough in wind has been in energy conversion. The older large wind turbines were AC syncronous machines, and had to sync to the power grid. That's why, when you see older wind farms like Pacheco Pass, all the blades are turning in sync. Modern units free-run, and there's an AC to DC to AC conversion with rectifiers and inverters to convert the output to 60Hz. This lowers the cut-in speed; with older systems, you couldn't get any power out until there was enough wind to get the generator up to 60Hz speed.
Software sucks because the costs of it sucking fall on the user, not the manufacturer. That's hasn't been true of automobiles for several decades now, and cars have gotten much better. When was the last time your car died on the road?
Many years ago, I was at Ford Aerospace when the Ford EEC-IV electronic engine control unit was being developed. In that unit, the program was permanent; it was in a mask-programmed device, and could not be changed without replacing the entire unit. Very substantial resources were devoted to insuring that there were no bugs that could cause cars to fail on the road. There was huge fear of a recall; if something had gone wrong, most of the Ford cars on the road would have to come back to a dealership for CPU replacement. There were old engineers at Ford who didn't want a computer to have direct control of the engine. Tweak the spark timing a bit or adjust the emissions valves, like the earlier models of engine control, perhaps. But actually fire the spark plug directly from software? That was radical. So everyone involved was paranoid about bugs.
It worked. Twenty years later, no bugs have been found. There was never an EEC-IV recall. The EEC-IV is still popular with enthusiasts. You can even download the code and run it in an emulator. I still have a 1985 Ford Bronco with its original EEC-IV, and it runs fine.
If Microsoft had to face the possibility of bringing every PC with Windows on it into an approved Microsoft repair center for a software update at Microsoft's expense, Windows would not crash. It might not do as much, but critical components of it wouldn't fail disasterously.
And that's why software sucks.
There are several pro-Israel monitoring services watching the press - CAMERA in the US, BICOM in the UK, and MEMRI to monitor the Arab press. CAMERA is noted for having a good database of stories about Israel. Apparently stories mentioning Israel are found automatically, but evaluated by people.
The CIA has something called the "Open Source Intelligence Service", which started as the "Foreign Broadcast Monitoring Service". Visualize some poor guy spending eight hours a day listening to Radio Albania, all through the Cold War. Most of the content is terminally boring, but then, one day the announcer says "so we're invading Yugoslavia", and the CIA needs to notice this. There have been repeated attempts to automate the job.
Wind turbines are only useful if the average wind speed is above 10 mph. The unit illustrated doesn't even cut in until 8 mph, and achieves its rated output at a wind speed of 20 mph.
Unless you're in an area with wind speeds like that, a wind turbine is a waste of time. Most people don't live in areas that windy; it's not comfortable. I've known people along the California coast who have useful wind turbines, but that's a special situation, where you have reliable medium-speed wind all year because of the ocean/land temperature difference. The serious California wind farms are in mountain passes or at desert/mountain boundaries, where the geography guarantees wind. Also, wind speeds are higher a few hundred feet up, which is why the really big wind machines on the high towers work even in flat terrain. A little turbine in your back yard probably is just going to sit there, stationary, most of the time.
If you're thinking of getting a wind turbine, put up a pole with one of those little "weather station" units that has an anemometer, and log wind speeds for a year. For a few hundred dollars, you'll find out if it's going to work.
If you can hang a wind chime outside your house and it doesn't drive you nuts with constant clanging, your location is not suitable for wind power.
This is the only post that sounds like it's coming from someone with a clue.
They made it "fanless", right? Fanless electronic devices with significant heat loads are inherently vulnerable; if the external environment is worse than the design spec, they die. Hot weather or tight shelf space, and you're dead.
Worse, if some systems are failing early in life due to cooling problems, more are very likely to fail later. ICs that run hot has a reduced lifespan; there's a well-understood relationship for this. So if demo units are failing when new, this is serious.
Somewhere at Sony, I suspect that engineers are frantically trying to tweak the heatsink, airflow, and case hole design before shipping. It's very late for that.
There will probably be aftermarket fan kits. Liquid cooling would be overdoing it.
That review reads like one of those suck-up reviews from a game mag supported by game advertising. Is this game advertised on Slashdot?
From the description, the game sounds like what, in the industry, is derisively called a "track ride", where you're led by the nose through a canned story.
Here's one of that Casio family. Other options (moving hands, metal cases, etc.).
I'm wearing one. It's a Casio watch which receives WWV. It sets itself every night at 2 AM. Knows the date. Adjusts for daylight savings time. Solar-powered, so it doesn't need battery replacement. So it doesn't need any attention. Lights up if you rotate your wrist rapidly. Waterproof and rugged enough to survive outdoor activities. Costs about $50.
This definitively solves the "what time is it" problem for locations in the United States. Anything beyond this is bling.
Bin Laden ordered Al-Qaeda to attack oil facilities several years ago. To date, the attacks consist of an attempt to drive two cars through the outer perimeter fence of a Saudi oil refinery. Two suicide bombers set off their explosives and started a small fire, which was quickly put out.
DARPA has been funding this kind of thing for years. Small turbines have resulted. DARPA was originally trying to develop bird-sized unmanned aerial vehicles. That R&D program produced some flyable devices, but they didn't have the low cost and 2-hour endurance DARPA wanted.
DARPA-funded work at MIT resulted in some microturbine parts back in 1997. Progress has been slower than expected, but it's happening.
The microgenerator thing was intended as a military application. The idea is to have something small, maybe even wearable, a soldier can use to recharge all the battery-operated gear. Battery recharging in the field, where power outlets are rare, is getting to be a huge hassle in the US military. Current technology is to put power outlets on everything with wheels and an engine, but that creates its own headaches.
Here's a list of offshore legal services. Now you can have your legal work done in Bangalore. Pass a copy of this to your corporate counsel.
But beyond the punditry, the big problem is that the US is losing manufacturing jobs. Most productivity growth is in manufacturing; productivity in services increases very slowly. Janitors and sales reps are barely more productive than they were decades ago.
The US is losing in high-tech products, too. For decades, the US exported far more high-tech products than it imported. That ended in 2002. Since then, imports have exceeded exports. And that's in high-tech; it's far, far worse in steel, textiles, general manufactured goods...
What's striking is how fast this has happened. There's been a huge change in the US economy since 2000. It's not a recession; it's a fundamental loss of productive capacity. Entire industries have disappeared in the US; textiles, paper, machine tools ... computers. Very few computers are actually made in the US.
This is finally getting attention because upper management is being "outsourced". First the manufacturing moves offshore. Then the engineering. Then the marketing operation becomes a small unit in Bentonville to interface with WalMart. Financing starts to come from Hong Kong and Dubai instead of New York.
At that point, there's no reason for expensive upper management in the US.
The IBM PC saga is instructive. It's Lenovo now. Principal operations are in Beijing. There's an "executive headquarters" in Raleigh, NC. They're hiring; they have about 250 openings. One is high-level technical (wireless networking interoperability). Five are low-level technical. The others are all sales-related, except for some people in "accounts receivable" doing collections.
Lenovo started out with more ex-IBM execs, but they're gradually disappearing.
Warren Slocum, who is in charge of elections here in San Mateo county, is extremely critical of touch-screen voting machines. He liked the system we had here - big paper ballots marked with black markers, which the voter inserts into the scanner atop the ballot box. This gives a quick count when the polls close, and the ballots are locked in the box in case a recount is needed.
But we couldn't keep that system. It wasn't compliant with the "Help America Vote Act", which requires touch-screen machines for "accessability" by blind people. San Mateo had to go touch-screen, but it went with Hart InterCivic eSlate machines. They're still not high-security devices, but they're way better than the Diebold crap. Slocum pushed to get California to require printers for manual recounts on all California touch-screen machines, and that's now the law in California.
But Hart InterCivic has problems, too.
"Gail Fisher, manager of the county's Elections Division (for Travis, TX), theorizes that after selecting their straight party vote, some voters are going to the next page on the electronic ballot and pressing "enter," perhaps thinking they are pressing "cast ballot" or "next page." Since the Bush/ Cheney ticket is the first thing on the page, it is highlighted when the page comes up - and thus, pressing "enter" at that moment causes the Kerry/ Edwards vote to be changed to Bush/ Cheney."
What CMU is selling (and yes, they're operating a business) is like those remote-controlled "entertainment robots" of the 1980s. There's apparently someone in the background running the thing. Big deal.
Now here's a useful entertainment robot - the MotoMan RoboBar This is a two-armed industrial robot bartender. For real.
The MotoMan RoboBar is from the leading robotics company from Japan, Yaskawa Electric. Over 120,000 robots installed. Their slogan is intimidating: "We already make your car. Let us make your drink". While CMU is making toys, Yaskawa is automating the world.
It's even worse. Look at the examples in the article. The upconverted versions have big rectangular compression artifacts. So not only were they upconverted, they were decompressed and recompressed, which generates terrible artifacts. (See most files on YouTube for examples.) If they'd just been upconverted from low-rez source material, they'd just be blurry.
No, this is the real article, three blogs down.
Lovin the LOLs, LOL is my will
MAYBE NONE OF, PROBABLY ALL OF, AND DEFINITELY MORE THAN:
New ways of getting your load onto your quivering victim's stack
Reaching into the hearts and minds (also the genitals) of users.
Firefox re-entrant threading lols
Patching BIOS for kernel-patching rootkit memory injections
Aggresive AIM attacks and escapades
Internet hilarity, sexual innuendo, LOLDONGS
Well, I'll say one thing for them. They put enough bandwidth behind the site that the video downloaded without any delays. Go ahead, watch the Quicktime version.
Not Roland the Plogger again? He just posted a crap story yesterday. This has to stop.
Here's the SCO vs IBM case schedule. Note how many key steps are now complete and in the past. Discovery is over. Expert reports are over. The final deadline for expert discovery passed last week. No more surprises. No more "secret evidence". No more stalling. We're past that. All the evidence is on the table now. The process grinds slowly, but it does grind.
Now the process speeds up. There's a significant deadline every few weeks now. Right now, summary judgement motions are being briefed and decided. That may end the case in favor of IBM, and it will almost certainly narrow it, as SCO's unsupported claims are knocked down. Those will be decided by the end of the year.
In January, the pace speeds up even more. As trial approaches, there are judge-set deadlines every few days.
If there's anything left to try, trial starts February 26, 2007. Not that far away.
The Internet Archive has an ongoing effort to measure disk drive reliability. They have several thousand disk drives for which they are collecting data, and for the year 2005, about 2% failed. This is better than previous years; a few years back they were experiencing 6%/year failure rates.
They send them back for warranty replacement, I'm told.
What is the semantic difference between C and Pascal?
The big problems with C/C++ from a formal methods standpoint:
I would expect pointer arithmetic to be the source of problems, but if I recall correctly, Pascal's pointers have arithmetic as well.
No, they don't.
Pointer arithmetic really is obsolete. Compilers have been generating code for subscripting that's as good or better than pointer arithmetic code for well over a decade now.
Even for Roland the Plogger, this is lame. Does he pay Slashdot to let him through, or what?
The main reason program verification didn't catch on was that it was hopeless for C and C++. The semantics of those languages were so messy that formalizing them was nearly hopeless.
Java and C#, however, are good enough. (So were Pascal, Modula, and Ada.)
Here's the manual for the Pascal-F verifier, a system written by a team I headed back in the early 1980s. This was a proprietary system done internally for Ford Motor Company. Take a look at the example real time engine control program beginning on page 155. It was painfully slow back then; it took 45 minutes of VAX 11/780 time (1 MIPS) to verify that program from a cold start. Today, it would take about a second.
What's being proved in that example? First, that there are no subscripts out of range or arithmetic overflows. Second, that all loops terminate. (Yes, you can prove that for most useful programs; the halting problem applies only to pathological programs.) Third, that the following constraints hold:
Useful stuff, the conditions needed to keep the engine running.
This is "design by contract" with teeth. Each function is checked to insure that it always satisfies its exit conditions if its entry conditions are satisfied by the caller, and that the function doesn't overflow, subscript out of range, or fail to terminate. Each call is checked to insure that its entry conditions are always satisfied. The end result is a guarantee that those properties hold for the whole program.
This is a very valuable check. It insures that caller and callee are in agreement on how to call each function. That's the cause of a huge number of software bugs - the caller made some incorrect assumption about the function being called, or the function didn't check for something which it needed to check. Both of those can be statically machine checked.
It's not easy to get a program through formal verification with a verifier like that one. The verifier does almost all the work on easy sections of code, but where correctness depends on anything non-trivial, you have to work with the theorem prover to get the proofs through. This isn't easy. The DEC Java checker and Microsoft's Spec# checker aren't as hard-line.