Re^4: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful)

in reply to Re^3: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful)
in thread An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful)

How much commercial code is ever formally proven? Effectively none.

Don't forget, open source code is as often not formally proven as commercial code!

And it shows. Nowhere except for software do people accept products that are so full of bugs and errors. If one car in 50,000 displays a warning light when it shouldn't, the manufacturer recalls millions of them. Just in case. When it comes to software, people can buy the next version, with a new set of bugs.

Comment on Re^4: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful)

Replies are listed 'Best First'.
Re^5: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful) by BrowserUk (Patriarch) on Sep 25, 2011 at 10:43 UTC
Don't forget, open source code is as often not formally proven as commercial code! Sorry. I cannot parse that sentence? Do you mean: open source code is as often as not formally proven as commercial code!? Or maybe: open source code is often not as formally proven as commercial code!? Actually, neither makes sense to me. Nobody formally proves software outside of academia. Even then, that small subset that are formally proven tend to be tiny snippets implementing convenient algorithms on idealised systems, with no time pressures, which if costed at commercial rates would be ruinously expensive. In reality, it doesn't matter, because when I use the phrase "commercial code" I mean code that is written to be used commercially, as opposed to code that is written for academic purposes; and that includes open source software. The nearest equivalents in the motor industry are those design prototypes that they show at events like the Geneva Motor Show, that never get into production. If one car in 50,000 displays a warning light when it shouldn't, the manufacturer recalls millions of them. Just in case. Great example, but wrong argument! I whole heartedly agree that the state of the software industry hasn't yet reached the maturity of the car industry when they were building Model T Fords; and I lamented the typical software disclaimers and what they say about this industry in Re^5: Programming is more like: Car designs aren't proven mathematically. They are tested. Often to destruction. As an example of the futility of trying to use maths as the ultimate design tool for cars, in late 2009 Virgin Racing set out in to design an F1 racing car using only Computational Fluid Dynamics. After two years and close to Ł100 million during which they rarely came anywhere but last, they recently announced that they were abandoning that policy and are going to rent expertise and facilities -- particularly wind tunnel time -- from one of their competitors. And cars, even F1 cars, probably have less "moving parts" than the (fairly modest) editor I use, and certainly far less complexity than the browser you are viewing this in. Examine what is said, not who speaks -- Silence betokens consent -- Love the truth but pardon error. "Science is about questioning the status quo. Questioning authority". In the absence of evidence, opinion is indistinguishable from prejudice.	[reply]

Replies are listed 'Best First'.

Re^5: An exploration of higher-level-language approaches to the "First all-zero row in an NxN matrix" problem (goto Considered Harmful)
by BrowserUk (Patriarch) on Sep 25, 2011 at 10:43 UTC

Don't forget, open source code is as often not formally proven as commercial code!

Sorry. I cannot parse that sentence?

Do you mean: open source code is as often as not formally proven as commercial code!?
Or maybe: open source code is often not as formally proven as commercial code!?

Actually, neither makes sense to me. Nobody formally proves software outside of academia. Even then, that small subset that are formally proven tend to be tiny snippets implementing convenient algorithms on idealised systems, with no time pressures, which if costed at commercial rates would be ruinously expensive.

In reality, it doesn't matter, because when I use the phrase "commercial code" I mean code that is written to be used commercially, as opposed to code that is written for academic purposes; and that includes open source software.

The nearest equivalents in the motor industry are those design prototypes that they show at events like the Geneva Motor Show, that never get into production.

If one car in 50,000 displays a warning light when it shouldn't, the manufacturer recalls millions of them. Just in case.

Great example, but wrong argument!

I whole heartedly agree that the state of the software industry hasn't yet reached the maturity of the car industry when they were building Model T Fords; and I lamented the typical software disclaimers and what they say about this industry in Re^5: Programming is more like:

Car designs aren't proven mathematically. They are tested. Often to destruction.

As an example of the futility of trying to use maths as the ultimate design tool for cars, in late 2009 Virgin Racing set out in to design an F1 racing car using only Computational Fluid Dynamics. After two years and close to Ł100 million during which they rarely came anywhere but last, they recently announced that they were abandoning that policy and are going to rent expertise and facilities -- particularly wind tunnel time -- from one of their competitors.

And cars, even F1 cars, probably have less "moving parts" than the (fairly modest) editor I use, and certainly far less complexity than the browser you are viewing this in.

Examine what is said, not who speaks -- Silence betokens consent -- Love the truth but pardon error.

"Science is about questioning the status quo. Questioning authority".

In the absence of evidence, opinion is indistinguishable from prejudice.

[reply]

In Section Meditations