On 25/09/17 18:58, Óscar Fuentes wrote: > Mario Castelán Castro writes: >> This depends on what exactly is meant by “correct”. > > "correct" means that the client (the people who required the software) > says that the program fulfills his requirements. Sometimes you need to > wait an infinite amount of time for obtaining client's approbation :-) The same answer applies: If a client either provides himself or accepts a formula in formal logic as a description of his requirements, then yes, we can prove that a program is correct according to this concept. If the client can not provide an *absolutely accurate* description (this is necessarily a specification in formal logic) of what his requirements are, then we can not assure the client that the program meets his requirements. This is not a fault of the programmer, but of the client for being vague about what his requirements are. >> If by “correctness” it is meant a formula in *formal logic*, then yes, >> we can prove that the program behaves correctly. > > Ever heard of a chap named Kurt Gödel? Or his cousin Alan Turing? :-) What you are doing here is intellectual fraud. You are conveying the impression that there is an obstacle that prevents formal verification, yet you did not even _mention_ what this obstacle is. Given that you mentioned Gödel, I guess (I can merely *guess* your intent because you did not explain it; this is your fault, not mine) that you believe that either the Gödel-Rosser incompleteness theorem[Mend, p. 210] or one of the many variations is an obstacle for formal verification. This is incorrect. What these theorems state is that in any formal system that meets certain prerequisites, there is an assertion P such that neither P nor ¬P are a theorem of the formal system. Also, it seems that you are confusing algorithmic undecidable problems (like the halting problem) with formally undecidability propositions (like the axiom of choice within ZF). In practice, using well-established logic systems (e.g.: HOL and ZFC) one does not _accidentally_ runs into formally undecidable statements. Moreover, suppose that you are “sure” that a certain proposition P that is undecidable in (say) HOL is “true”. What should you do? Since you are sure that P is “true”, then you must have proved P it in _some_ formal system (otherwise your claim has no logical basis) and you trust that this formal system is consistent. You can then either embed your formal system within HOL, or add the appropriate axioms (both options are a routine procedure in most proof assistants), and then prove P within your embedding in HOL or within your HOL+axioms system. Also, it is dubious whether it is a good idea to write a program whose correctness depends on baroque axioms like large cardinals. This commentary holds regardless of whether you are interested in formally proving its correctness. > […] it > is almost certain that there are "correct" informal specifications that > do not admit a verifiable formal specification. This is yet more intellectual fraud (an unjustified claim). > […] We must provide what is requested from us, in > terms of functionality, performance and cost […] Somebody has to take a decision between cheap software and reliable software. Those are mutually exclusive. The predominating choice is cheap software. As evidence for this claim I note the very high frequency of bug reports including security vulnerabilities. ***** I have spent already enough time addressing your misconceptions. If you reply to this message with even more misconceptions, I will not reply because I am unwilling to spend even more time explaining what you should already know. It is *YOUR* task to make sure you know what you are talking about (and you have failed so far), not mine!. If you are interested in formal logic, either because of genuine interest or just to criticize, I suggest [Mend] as a starting point. [Mend] E. Mendelson “Introduction to Mathematical Logic”, 6th edition (2015). -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan