Re: Intervention needed?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 2019-03-28 08:01, Maciej Sobczak wrote:

> Which brings a potentially interesting question - what if the reasoning in my head has a continuous measure of correctness? Like, say, I'm 95% confident that the reasoning is correct?

This is not how reasoning work. It is how the physical model does. 
Physical models have stochastic nature. The probabilistic measure is 
additive. But human reasoning is nowhere stochastic.

> Should I deploy my system or not? The mechanical proof will fail 100% of the time, but that does not mean that the software is entirely useless for my user, who also has his own continuous measure of risk and level of failure acceptance.

Nothing like that. You have states the physical system may go into with 
different probabilities. Some of these states are fail-states. It has 
nothing to do with proofs. If something is proven about a physical 
system, that would be a fact, not a statistical event. Fact /= event.

BTW, a digital system has an advantage that you can (theoretically) 
ensure some states never entered. You cannot do that with a physical 
system, there is always a non-zero probability that it would do nobody 
knows what.

> The ability to work with continuous measures is what is practiced in every other engineering discipline (including critical ones!), yet the formal-method priests like you prevent me from deploying my acceptably correct programs. I find it a *limitation* of your methods, not mine.

This again has nothing to do with measures, but with the Newtonian 
mechanics with limited masses and accelerations. The solutions there are 
smooth. Small changes of inputs produce small changes of outputs, except 
for few cases of chaotic systems etc.

These premises do not apply to digital systems. Programming languages 
like Ada are designed in a way to smooth the behavior a bit, in order to 
allow gradual design, but only a bit.

> Could you please fix your methods so that I can deploy my almost-certainly-correct system, like everybody else does, instead of forcing me to use tools that are demonstrably unfit for today's market needs? Thank you.

Very bad. This is a part of the problem as well. You cannot have it this 
way because old rules do not apply. Attempts to use quality assurance 
methods known in engineering disciplines to software result in 
nonsensical standards and certification procedures which assure nothing 
but wasting human resources.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de