4 ms·

Probably because the cost associated with constructing such proofs for the vast majority of modern software use cases (like showing ads on 8 different browsers)

Probably because the cost associated with constructing such proofs for the vast majority of modern software use cases (like showing ads on 8 different browsers) is too high (cheaper to just hire QA teams), and most programmers are not simultaneously software engineers, computer scientists, and mathematicians.

rramadass 6y ago
> cost associated with constructing such proofs ... is too high People assume this is true because it has been repeated endlessly. I think it is an issue of granularity. For example; both Dijkstra's GCL and Hoare's Triples (fine granularity) vs. Meyer's DbC (coarse granularity) can be expressed using Assertions to build Preconditions/Postconditions/Invariants as "correctness proof" throughout a real-world software system. But their systematic usage is never taught nor enforced; we have to learn it by trial and error.
- ativzzz 6y ago
  You really just made my point with your response > For example; both Dijkstra's GCL and Hoare's Triples (fine granularity) vs. Meyer's DbC (coarse granularity) can be expressed using Assertions to build Preconditions/Postconditions/Invariants as "correctness proof" throughout a real-world software system The average dev at an average company will read this and not understand 90% of your sentence. Again, the vast majority of devs are not computer scientists nor mathematicians. They are good at what they do, which is building what their bosses ask for using whatever web framework they specialize in.
  - rramadass 6y ago
    I think you are giving too little credit to the "average programmer's" intelligence. He/She is after all a self-learning, problem solving biological machine :-) An organisation that treats its programmers as morons will soon have programmers that are willing and able to act like morons only. -- Bjarne Stroustrup We all were "average programmers" at one time and didn't know better. But at some point some of us came to know(from whatever source) of a "better and correct way" of doing things and then realized that this should have been taught from the beginning. It is not enough to just teach people the syntax of a language and let them loose on the World; we have to be taught "discipline" and how to use it "correctly". In the context of this thread, that was exactly what Dijkstra strongly advocated for (see my other reply to you listing some paragraphs from EWD288). References (Wikipedia is a good starting point though sometimes overly complicates simple ideas): * Dijkstra's GCL - https://en.wikipedia.org/wiki/Guarded_Command_Language https://en.wikipedia.org/wiki/Guarded_Command_Language * Hoare's Triples - https://en.wikipedia.org/wiki/Hoare_logic https://en.wikipedia.org/wiki/Hoare_logic * Meyer's DbC - https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Design_by_contract * Assertions/Preconditions/Postconditions/Invariants - https://en.wikipedia.org/wiki/Assertion_(software_development) https://en.wikipedia.org/wiki/Assertion_(software_developmen... - https://en.wikipedia.org/wiki/Precondition https://en.wikipedia.org/wiki/Precondition - https://en.wikipedia.org/wiki/Postcondition https://en.wikipedia.org/wiki/Postcondition - https://en.wikipedia.org/wiki/Invariant_(mathematics)#Invariants_in_computer_science https://en.wikipedia.org/wiki/Invariant_(mathematics)#Invari...
rramadass 6y ago
Addendum to my previous reply from the end of EWD288 - "Concern for Correctness as a Guiding Principle for Program Composition"; My thesis is, that a helpful programming methodology should be closely tied to correctness concerns. I am perfectly willing to admit that I myself may be the most complete victim of my own propaganda, but that will not prevent me from preaching my gospel, which is as follows. When correctness concerns come as an afterthought and correctness proofs have to be given once the program is already completed, the programmer can indeed expect severe troubles. If, however, he adheres to the discipline to produce the correctness proofs as he programs along, he will produce program and proof with less effort than programming alone would have taken. The framework of this contribution does not allow the inclusion of a worked-out example. Instead I shall try to sketch how the hand-in-hand construction of a program and its correctness proof guides the programming process. I found what I regard as the quintessence of this methodology in the summer of 1968, when my attitude towards flowcharts changed radically. Up till that moment, I had regarded a flowchart as something incomplete, as a plan, as a (half-pictorial, but that is not essential) representation of my intentions, something that as a description would only make sense if all further details, down to the bottom, had indeed been supplied. But it was then that I saw that such a sketch of a program still to be made, could be regarded as an abstract version of the final program, or even, that it could be regarded as "the program", be it for a —in all probability hypothetical— machine with the proper repertoire of primitive actions operating on variables of the proper types. If such a machine were available, the "rough sketch" would solve the problem; usually it is not available, and actions and data types assumed have to be further detailed in the next levels of refinement. It is the function of these next levels to build the machine that has been assumed to be available at the top level, i.e. at the highest level of abstraction. This most abstract version is now no longer a draft of the final program, it is an essential part of the total program; its correctness is independent of the lower level refinements and can be established beforehand. To give this correctness proof before proceding with the lower level refinements serves many purposes. It establishes the correctness of the top level. Fine, but what is more important is that we do this by applying well-established theorems applicable to well-known sequencing clauses, and as a result it becomes most natural to avoid clever constructions like the plague. But the most important consequence is that the proof for one level ensures that the interface between itself and the lower levels has been given completely, as far as is relevant for that level; and also, by fixing in the interface only what the correctness proof really needs, the interface can be kept free from overspecification. Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels. In the step-wise approach it is suggested that even in the case of a well-defined task, certain aspects of the given problem statement are ignored at the beginning. This means that the programmer does not regard the given task as an isolated thing to be done, but is invited to view the task as a member of a whole family; he is invited to make the suitable generalizations of the given problem statement. By successively adding more detail in the lower levels he eventually pins his program down to a solution for the given problem.

rramadass 6y ago

> cost associated with constructing such proofs ... is too high People assume this is true because it has been repeated endlessly. I think it is an issue of granularity. For example; both Dijkstra's GCL and Hoare's Triples (fine granularity) vs. Meyer's DbC (coarse granularity) can be expressed using Assertions to build Preconditions/Postconditions/Invariants as "correctness proof" throughout a real-world software system. But their systematic usage is never taught nor enforced; we have to learn it by trial and error.

ativzzz 6y ago
You really just made my point with your response > For example; both Dijkstra's GCL and Hoare's Triples (fine granularity) vs. Meyer's DbC (coarse granularity) can be expressed using Assertions to build Preconditions/Postconditions/Invariants as "correctness proof" throughout a real-world software system The average dev at an average company will read this and not understand 90% of your sentence. Again, the vast majority of devs are not computer scientists nor mathematicians. They are good at what they do, which is building what their bosses ask for using whatever web framework they specialize in.
- rramadass 6y ago
  I think you are giving too little credit to the "average programmer's" intelligence. He/She is after all a self-learning, problem solving biological machine :-) An organisation that treats its programmers as morons will soon have programmers that are willing and able to act like morons only. -- Bjarne Stroustrup We all were "average programmers" at one time and didn't know better. But at some point some of us came to know(from whatever source) of a "better and correct way" of doing things and then realized that this should have been taught from the beginning. It is not enough to just teach people the syntax of a language and let them loose on the World; we have to be taught "discipline" and how to use it "correctly". In the context of this thread, that was exactly what Dijkstra strongly advocated for (see my other reply to you listing some paragraphs from EWD288). References (Wikipedia is a good starting point though sometimes overly complicates simple ideas): * Dijkstra's GCL - https://en.wikipedia.org/wiki/Guarded_Command_Language https://en.wikipedia.org/wiki/Guarded_Command_Language * Hoare's Triples - https://en.wikipedia.org/wiki/Hoare_logic https://en.wikipedia.org/wiki/Hoare_logic * Meyer's DbC - https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Design_by_contract * Assertions/Preconditions/Postconditions/Invariants - https://en.wikipedia.org/wiki/Assertion_(software_development) https://en.wikipedia.org/wiki/Assertion_(software_developmen... - https://en.wikipedia.org/wiki/Precondition https://en.wikipedia.org/wiki/Precondition - https://en.wikipedia.org/wiki/Postcondition https://en.wikipedia.org/wiki/Postcondition - https://en.wikipedia.org/wiki/Invariant_(mathematics)#Invariants_in_computer_science https://en.wikipedia.org/wiki/Invariant_(mathematics)#Invari...

rramadass 6y ago

Addendum to my previous reply from the end of EWD288 - "Concern for Correctness as a Guiding Principle for Program Composition"; My thesis is, that a helpful programming methodology should be closely tied to correctness concerns. I am perfectly willing to admit that I myself may be the most complete victim of my own propaganda, but that will not prevent me from preaching my gospel, which is as follows. When correctness concerns come as an afterthought and correctness proofs have to be given once the program is already completed, the programmer can indeed expect severe troubles. If, however, he adheres to the discipline to produce the correctness proofs as he programs along, he will produce program and proof with less effort than programming alone would have taken. The framework of this contribution does not allow the inclusion of a worked-out example. Instead I shall try to sketch how the hand-in-hand construction of a program and its correctness proof guides the programming process. I found what I regard as the quintessence of this methodology in the summer of 1968, when my attitude towards flowcharts changed radically. Up till that moment, I had regarded a flowchart as something incomplete, as a plan, as a (half-pictorial, but that is not essential) representation of my intentions, something that as a description would only make sense if all further details, down to the bottom, had indeed been supplied. But it was then that I saw that such a sketch of a program still to be made, could be regarded as an abstract version of the final program, or even, that it could be regarded as "the program", be it for a —in all probability hypothetical— machine with the proper repertoire of primitive actions operating on variables of the proper types. If such a machine were available, the "rough sketch" would solve the problem; usually it is not available, and actions and data types assumed have to be further detailed in the next levels of refinement. It is the function of these next levels to build the machine that has been assumed to be available at the top level, i.e. at the highest level of abstraction. This most abstract version is now no longer a draft of the final program, it is an essential part of the total program; its correctness is independent of the lower level refinements and can be established beforehand. To give this correctness proof before proceding with the lower level refinements serves many purposes. It establishes the correctness of the top level. Fine, but what is more important is that we do this by applying well-established theorems applicable to well-known sequencing clauses, and as a result it becomes most natural to avoid clever constructions like the plague. But the most important consequence is that the proof for one level ensures that the interface between itself and the lower levels has been given completely, as far as is relevant for that level; and also, by fixing in the interface only what the correctness proof really needs, the interface can be kept free from overspecification. Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels. In the step-wise approach it is suggested that even in the case of a well-defined task, certain aspects of the given problem statement are ignored at the beginning. This means that the programmer does not regard the given task as an isolated thing to be done, but is invited to view the task as a member of a whole family; he is invited to make the suitable generalizations of the given problem statement. By successively adding more detail in the lower levels he eventually pins his program down to a solution for the given problem.