Big Case

Opening Contention

Presumably from Big CASE (Computer Aided SoftwareEngineering - see also CaseTool). The ProjectManagement HolyGrail of the methodology, language (e.g. Ada) or CaseTool that can make a SoftwareEngineering project produce a "guaranteed correct" product, has been around for a long time.

However ComputerScience, specifically the ChurchTuringThesis, has long ago demonstrated mathematically (or has it?) that it is impossible to prove the correctness or "bug-free" nature of any reasonably-sized or complex software project.

-- PaulBowman

Big CASE in the real world...

This was one of the reasons why when the Reagan administration announced that their "Star Wars" program was going to consist of a satellite network of fission-powered x-ray cannons controlled by a million lines of "guaranteed correct" code, computer scientists the world round shook their heads in despair and wonder at the gullibility of, not the general public per se, but the self-declared "opinion formers" who are supposed to inform the general public when their leaders are talking pure baloney (but somehow never do).

(Re-factor at will with one caveat: the Star Wars I point was one we covered in Computational Theory at Leeds University, not just a personal bugbear - I am not alone in maintaining that it stands. Plus with Star Wars II being threatened it is still a contemporary issue, not merely historical)

Objection

It is false that ComputerScience, specifically the ChurchTuringThesis, has long ago demonstrated mathematically that it is impossible to prove the correctness or "bug-free" nature of any reasonably-sized or complex software project. What has been demonstrated is that arbitrary programs cannot be proven complete or bug-free. By developing the proof(s) along with the program(s), very large systems have been produced that have been proven bug-free given the assumptions of the system.

You may choose to dispute the assumptions, you may raise concerns over the correctness of the specification or of the hardware used to implement the system, but the ChurchTuringThesis talks about the impossibility in general of proving arbitrary programs correct.

As a related side-issue, most examples of NP-complete problems are trivial to solve in polynomial using existing algorithms. What is impossible is to solve arbitrary problems in polynomial time. It is widely believed that the difficult examples form a vanishingly small proportion of the collection.

I strongly believe that sweeping statements such as yours are a major stumbling block in the advancement of the science of programming.

If I understand correctly you are affirming that the goal of BigCASE is not incompatible with the ChurchTuringThesis (leaving aside all emotive questions on the wisdom of entrusting the salvation of humanity from nuclear holocaust to a US DoD software project ;). This is obviously an important question for software engineering. But to support/expand your thesis can you...

define arbitrary and its converse non-arbitrary in your re-statement of the ChurchTuringThesis (henceforth CTT)?
expand on the significance of emphasising in general in relation to CTT?
explain why the caveat "given the assumptions of the system" is not just circularity or begging the question?
(for pedagogic purposes) give us the best link to explain NpComplete?

Hopefully with all of the above we can refactor this into a useful exploration of the software engineering relationship to the CTT.

Finally,

: > I strongly believe that sweeping statements such as yours are a major stumbling block in the advancement of the science of programming.

If those statements are made with strong authority through inegalitarian or one-way communications media, then I would agree. However, in a collaborative space of a Wiki they can be handy in flushing out lurkers (such as yourself) who can add to what UncleCharlie called the GeneralIntellect. Agreed - my annoyance/anger is aimed at the self-satisfied pedagogues (spelling?) who are simply wrong.

In this context:

: arbitrary programs cannot be proven complete or bug-free

"arbitrary" means "any given". You cannot guarantee to prove correct any given program. The converse is that if you choose the program sufficiently carefully then you can prove it complete. You're not being asked to do it for just any old program, you're allowed to put conditions on it. Your conditions don't have to be that it's small or toy, your conditions can be that it's well-written and has the proof of correctness developed as part of the writing. In this way programs of arbitrary size (that is - you say how big and I can meet that requirement) can be written and proven correct.

The "in general" is the same point. Programs in general cannot be proven correct. Specific programs can be proved correct, even very big and very complex programs can be proven correct.

The caveat of "given the assumptions of the system" allow you to limit the scope and avoid proving that the hardware is correct, that the specification is correct, etc. These are important additional issues, but they are additional issues. Proving program correctness is an important issue that can and should be addressed separately first, and then considered in the wider context of the system as a whole.

NpComplete is hard. The page here is pretty good, but hasn't really settled into proper DocumentMode yet. Specific questions here might be better after reading that page.

It's true that programs in the real world are rarely proven correct, and that there is a trade-off that suggests that it's never worth-while. That doesn't mean it's impossible. It doesn't even mean that it's really, really, really hard.

Query: Is your position founded on formal theoretical/mathematical investigation or can you point us to real-world methodologies or languages which try to bridge the gap for software engineering projects? (PB)