5 ms·

I am afraid you have not really understood the mathematical theory and its mapping to programming. Relational Algebra doesn't just mean RDBMS/SQL but is a gener

I am afraid you have not really understood the mathematical theory and its mapping to programming. Relational Algebra doesn't just mean RDBMS/SQL but is a general algebra where algebraic Operations are defined over mathematical Relations i.e. over a Cartesian Product of one or more Sets. As a first approximation; a) Type = Set b) Function = subset of Relation (i.e. set of Tuples) obtained from Cartesian Product of {input type set X output type set} c) Logical conditions define new relational sets where its members have a ordering relation d) A Program is a series of functions which prune and transform the tuples from the above cartesian product.

cubefox 1y ago
Well, I'm familiar with model theory and Church's simple theory of types, but I don't think things like that are useful in practice. Perhaps the concept of currying would be an exception, if I were a Haskell programmer.
- rramadass 1y ago
  I am not sure that you have really understood the topics you have named. All high-level programming languages give you a set of fundamental types and the ability to construct user-defined types. Currying is not an exception but falls under the same model if one considers it as a Relation between "sets of functions". Also by Curry-Howard correspondence you have "formula/proposition = type" and "proof = function". So you have a direct mapping between Sets/Relations/Logic in Mathematics and Types/Logic in a Program. A Program then becomes a trajectory enforced using predicate logic through a state space obtained from the cartesian product of all the types in the program. You are using all of the above whether you know it or not when programming in a high-level language. The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification).
  - elderhammer 1y ago
    [dead]
  - cubefox 1y ago
    > You are using all of the above whether you know it or not when programming in a high-level language. Exactly. The average programmer doesn't have to know the math behind things like types to use them. > The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification). I don't think the average software engineer does that or would benefit from doing it. I certainly don't.
    - rramadass 1y ago
      > I don't think the average software engineer does that or would benefit from doing it. I certainly don't. Again; you are drawing the wrong conclusions and projecting your own ignorance on others. To give a simple analogy; anybody can swing a baseball bat at a ball. But that won't make him a notable player. To become a superlative player one needs to understand body dynamics and train scientifically. In a similar vein, anybody can muddle through and come up with a Program. But more often than not, it will be error-prone and bug-ridden not to mention hard to extend and maintain. Given the importance of Software to our modern society this is not what we want. A little bit of knowledge of Mathematics behind Programming gives you orders of magnitude return in software quality which is absolutely worthwhile. There is nothing to debate/argue here but merely pointing out the application of scientific method to software engineering.
      - cubefox 1y ago
        > Again; you are drawing the wrong conclusions and projecting your own ignorance on others. I reject your accusation. It's more likely that you are the one who is projecting, namely your ignorance of what the average software engineer is doing.
        rramadass 1y ago
        Your opinion has zero basis in facts and betrays some serious ignorance of Scientific Method. No educated person can deny the importance of Mathematics to our technologically advanced society today. Computer Science is a subfield of Mathematics and Computer Programming is the application of principles and concepts studied therein. As mentioned earlier, the point of studying Mathematics for Computer Science is to make your "average software engineer" better and more productive than he/she was in the past. Eugene Wigner's classic essay The Unreasonable Effectiveness of Mathematics in the Natural Sciences is very relevant here - https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness_of_Mathematics_in_the_Natural_Sciences https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness...
  - MaxBarraclough 1y ago
    > The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification). At the risk of nitpicking: Certainly it's a benefit to structure and understand code such that you can reason about it effectively, but prove goes too far. Almost no real code is proven correct, the ergonomics of formal methods are still far too poor for that.
    - rramadass 1y ago
      It depends; the "proving" can be done at a gross high level function or fine grained at statement level. Thus in the former case one could use Meyer's Design-by-Contract (aka DbC) while in the latter case one might choose to follow a detailed Dijkstra methodology. For both of the above you don't need any special tools (eg. Z/VDM/TLA+/Coq/Lean etc.) but merely the knowledge to learn to think about a Program using Mathematical Concepts. For most "ordinary" software, DbC would be enough while for critical software one might want to go with the whole nine yards using chosen methodologies/tools. Note that usage of the methodologies/tools themselves require a knowledge of the above-mentioned Mathematics. The point was that a knowledge of the requisite Mathematics gives you a very powerful way of viewing Programs and then you get to choose how to map/implement it using any number of tools and based on the needs of the software.
      - MaxBarraclough 1y ago
        Design-by-contract typically refers to runtime checking of invariants, which is not the equivalent of formal verification. It should not be referred to as proving correctness. It doesn't do so. If you want to prove your program's correctness, that's the domain of formal methods, essentially by definition.
        rramadass 1y ago
        This argument has been made before and that is why i said it depends and put "proving" within quotes. It is a very narrow and wrong way of looking at Formal Methods (both Specification and Verification) and one of the main reasons the "ordinary" software engineer gets intimidated and overawed by formal methods and afraid to even approach the subject (as my comments to user cubefox shows). A Formal Method defined broadly is the application of Mathematical Concepts/Models and Logic to the specification/implementation/verification of Computer Programs. DbC is based on Hoare Logic where you try to "prove" the program intellectually and not necessarily tool driven. This was somewhat mechanized (though still a intellectual pursuit) by Dijkstra's technique of deriving weakest-preconditions. Because the whole process can be quite tedious, laborious and rather complex, automatic theorem prover tools were invented to do the job for you. This has resulted in the unfortunate status quo where Formal Specification/Verification have become identified with the use of tools and not the Mathematics behind them. Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools. DbC can be considered a lightweight Formal Method with aspects of both Specification and Verification included. The Programmer plays the role of "theorem prover" when using DbC. However tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs. See for example https://www.eschertech.com/products/verified_dbc.php https://www.eschertech.com/products/verified_dbc.php. Also Eiffel (quintessential DbC language) can be converted using AutoProof to a form which can be proven by Boogie verifier. Finally; here is a case study Design by contract formal verification for automotive embedded software robustness (abstract & pdf) - https://hal.sorbonne-universite.fr/ERTS2024/hal-05028176v1 https://hal.sorbonne-universite.fr/ERTS2024/hal-05028176v1

cubefox 1y ago

Well, I'm familiar with model theory and Church's simple theory of types, but I don't think things like that are useful in practice. Perhaps the concept of currying would be an exception, if I were a Haskell programmer.

rramadass 1y ago
I am not sure that you have really understood the topics you have named. All high-level programming languages give you a set of fundamental types and the ability to construct user-defined types. Currying is not an exception but falls under the same model if one considers it as a Relation between "sets of functions". Also by Curry-Howard correspondence you have "formula/proposition = type" and "proof = function". So you have a direct mapping between Sets/Relations/Logic in Mathematics and Types/Logic in a Program. A Program then becomes a trajectory enforced using predicate logic through a state space obtained from the cartesian product of all the types in the program. You are using all of the above whether you know it or not when programming in a high-level language. The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification).
- elderhammer 1y ago
  [dead]
- cubefox 1y ago
  > You are using all of the above whether you know it or not when programming in a high-level language. Exactly. The average programmer doesn't have to know the math behind things like types to use them. > The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification). I don't think the average software engineer does that or would benefit from doing it. I certainly don't.
  - rramadass 1y ago
    > I don't think the average software engineer does that or would benefit from doing it. I certainly don't. Again; you are drawing the wrong conclusions and projecting your own ignorance on others. To give a simple analogy; anybody can swing a baseball bat at a ball. But that won't make him a notable player. To become a superlative player one needs to understand body dynamics and train scientifically. In a similar vein, anybody can muddle through and come up with a Program. But more often than not, it will be error-prone and bug-ridden not to mention hard to extend and maintain. Given the importance of Software to our modern society this is not what we want. A little bit of knowledge of Mathematics behind Programming gives you orders of magnitude return in software quality which is absolutely worthwhile. There is nothing to debate/argue here but merely pointing out the application of scientific method to software engineering.
    - cubefox 1y ago
      > Again; you are drawing the wrong conclusions and projecting your own ignorance on others. I reject your accusation. It's more likely that you are the one who is projecting, namely your ignorance of what the average software engineer is doing.
      - rramadass 1y ago
        Your opinion has zero basis in facts and betrays some serious ignorance of Scientific Method. No educated person can deny the importance of Mathematics to our technologically advanced society today. Computer Science is a subfield of Mathematics and Computer Programming is the application of principles and concepts studied therein. As mentioned earlier, the point of studying Mathematics for Computer Science is to make your "average software engineer" better and more productive than he/she was in the past. Eugene Wigner's classic essay The Unreasonable Effectiveness of Mathematics in the Natural Sciences is very relevant here - https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness_of_Mathematics_in_the_Natural_Sciences https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness...
- MaxBarraclough 1y ago
  > The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification). At the risk of nitpicking: Certainly it's a benefit to structure and understand code such that you can reason about it effectively, but prove goes too far. Almost no real code is proven correct, the ergonomics of formal methods are still far too poor for that.
  - rramadass 1y ago
    It depends; the "proving" can be done at a gross high level function or fine grained at statement level. Thus in the former case one could use Meyer's Design-by-Contract (aka DbC) while in the latter case one might choose to follow a detailed Dijkstra methodology. For both of the above you don't need any special tools (eg. Z/VDM/TLA+/Coq/Lean etc.) but merely the knowledge to learn to think about a Program using Mathematical Concepts. For most "ordinary" software, DbC would be enough while for critical software one might want to go with the whole nine yards using chosen methodologies/tools. Note that usage of the methodologies/tools themselves require a knowledge of the above-mentioned Mathematics. The point was that a knowledge of the requisite Mathematics gives you a very powerful way of viewing Programs and then you get to choose how to map/implement it using any number of tools and based on the needs of the software.
    - MaxBarraclough 1y ago
      Design-by-contract typically refers to runtime checking of invariants, which is not the equivalent of formal verification. It should not be referred to as proving correctness. It doesn't do so. If you want to prove your program's correctness, that's the domain of formal methods, essentially by definition.
      - rramadass 1y ago
        This argument has been made before and that is why i said it depends and put "proving" within quotes. It is a very narrow and wrong way of looking at Formal Methods (both Specification and Verification) and one of the main reasons the "ordinary" software engineer gets intimidated and overawed by formal methods and afraid to even approach the subject (as my comments to user cubefox shows). A Formal Method defined broadly is the application of Mathematical Concepts/Models and Logic to the specification/implementation/verification of Computer Programs. DbC is based on Hoare Logic where you try to "prove" the program intellectually and not necessarily tool driven. This was somewhat mechanized (though still a intellectual pursuit) by Dijkstra's technique of deriving weakest-preconditions. Because the whole process can be quite tedious, laborious and rather complex, automatic theorem prover tools were invented to do the job for you. This has resulted in the unfortunate status quo where Formal Specification/Verification have become identified with the use of tools and not the Mathematics behind them. Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools. DbC can be considered a lightweight Formal Method with aspects of both Specification and Verification included. The Programmer plays the role of "theorem prover" when using DbC. However tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs. See for example https://www.eschertech.com/products/verified_dbc.php https://www.eschertech.com/products/verified_dbc.php. Also Eiffel (quintessential DbC language) can be converted using AutoProof to a form which can be proven by Boogie verifier. Finally; here is a case study Design by contract formal verification for automotive embedded software robustness (abstract & pdf) - https://hal.sorbonne-universite.fr/ERTS2024/hal-05028176v1 https://hal.sorbonne-universite.fr/ERTS2024/hal-05028176v1