Correctness.

Introduction.

Proving code's correctness / pl: dowodzenie poprawności kodu / can be done, but is very difficult & expensive so far.

Depending on purpose, code's correctness proofs are neccessary / for example: the nuclear reactor's software, airplane controls /, or not / for example: a non-commercial webpage /.

In reality, automated tests are enough for many applications, and proofs are used only in mission - critical software parts, because of the costs measured in programmers' work time and in other resources.

Too often even the simple automated tests are omitted in programmers' work - as customers mistakenly think that it costs less to just pay for bugfixing, than to pay for quality. But customers often lack knowledge neccessary to check code's quality, so they prefer to not pay for quality, while expecting it still.


Causal Proofs.

... i think that with coming of the 'Causal Programming Paradigm', proving code's correctness might become easier, automated testing as well.

With this paradigm, software analysis will be similar to observing a space - play, a play of causes & conditions.

Computation is calculation with side effects, depending on hardware & software, machines can compute either well or not so well.

In the Causal Programming Paradigm, cause's result appears when cause appears and conditions exist for long enough after cause's appearance.

Program's result is achieving certain results - either once, or continually, over a given time.

Idea of algorithm's correctness proof, therefore, is proving that a proper cause will appear, and proper conditions will exist for long enough, in a given timeframe.


See also, if You wish: Causes & Conditions.


Concurrency & Real Time.

Timeframe can be counted either using Real Time Clock, in case of Realtime programming languages, or defined as 'within brackets' of causes, countercauses, conditions and counterconditions appearance, existence or disappearance - in case of programming languages without Realtime mechanisms, as for example: 'Ola' Programming Language.

In a Nonrealtime Concurrent Systems, Real Time Clock can be used as well, but not so precisely.

Concurrency is not the same as Realtime Support Mechanisms, and considering either or both is not a small cost when proving program's correctness. In simpler words: Nonrealtime Concurrent Systems are faster usually than Realtime Concurrent Systems, but lack the Hard Pessimistic Time Constraints - often work faster, but occasionally are too slow. Realtime systems, when written correctly, do not fail at all - but are slower on average.

Nonrealtime Concurrent Systems are also cheaper and easier in making than Realtime Concurrent Systems, and market niche for these languages is much larger. People do not need expensive and over-ambitious solutions for most of simpler tasks, afterall.

Both the Realtime Concurrent Systems, as well as the Nonrealtime Concurrent Systems can work in Real Time, can have user interface that affect their behaviour. The 'Starcraft 2' Computer Game by Blizzard Entertainment is an example of the Nonrealtime Concurrent Program masterpiece - it works smooth and fast, but occassinally 'hiccups' - slows down for a while. Being a Nonrealtime Program it's much cheaper, and is faster on average.

'Starcraft 2' is the game of the 'RTS' - 'Real Time Strategy' Computer Games Genre, as it works in Real Time, Concurrently coordinating software parts. By the Computer Sciences Linguistics it is not a Realtime System, however, as it doesn't adhere to Pessimistic Time Contraints of the Realtime Systems. There's the difference between Computer Science's 'Realtime' meaning and the Common Sense's 'Real Time' meaning. The RTS Computer Game Genre illustrate this difference well enough, i think.


Quality & Professional Practices.

In formal proofs of program's correctness, minimalism is important too, code should have as little of side-effects as possible - only desired ones, if possible - as unwanted side effects, causes & conditions, can complicate proofs or interfere with results.

'The less code the better', SOLID, DRY / 'Don't repeat yourself' / & other ideas are important when considering 'Code Quality Metrics'.


Links.

See also, if You wish:
* Invariants,
* Causal Notation.