8 ms·

>Writing software is not math. You're wrong, and I've explained this upthread. >Think about food recipes. Do you have experience with non-imperative programm

by jolux 9y ago

>Writing software is not math. You're wrong, and I've explained this upthread. >Think about food recipes. Do you have experience with non-imperative programming paradigms? I'm sorry to say that the comparison to recipes in this context seems fairly naive. >People have been chasing the unicorn of software correctness proofs for 60 years, with a notable lack of generalizable success (there are plenty of toy examples, of course). Static type systems are arguably a product of this, especially advanced ones like Haskell's. >What usually happens is that the "programming is math" people come up with some bizarre academic language that no real-world programmer would use unless forced to do so at gunpoint (followed by the new language sinking without a trace). Now you're just being anti-intellectual. The whole point is that the real-world programmers are stumbling into all this crap constantly without realizing it. It's completely fucking unavoidable and very much tied up with the fact that programming is math. The only question is what you choose to do about that: learn the math, or stay ignorant. I don't mean to be condescending but I find comparing UML diagrams and proof assistants a little offensive (among other things), and it suggests you don't know what you're talking about. Modern proof assistants and other formal techniques like dependent typing happen while you're programming (Idris/Agda) or generate programs themselves (Coq), they aren't some sort of Waterfall-ish thing where you have to deal with all the ceremony before you start to get shit done. On the contrary, you get shit done, and it works better when you're done with it too.

hueving 9y ago
Your post contains a lot of unnecessary aggression. Rather than suggesting someone "doesn't know what they're talking about", just provide evidence to the contrary. That aside, there seems to be something missing in your analysis, or there would be a lot of successful startups stealing the market using proof assistants and formal techniques. It's not anti intellectual to point out that programmers don't want to use academic languages that have poor usability, steep learning curves, and garbage for standard libraries. Consider when a regular house is being built. There are many problems that could be avoided if an engineering firm spent an entire year analyzing the designs and their interactions with the target site. However, that's not done because it takes significantly longer and costs obscene amounts of money. It's easier for the construction crew to fix problems as they encounter them and for the owner to do repairs on the house 40 years later. Yeah, the house isn't as reliable, but it cost 100,000 instead of 1,000,000. If you want developers and managers on your side, you need to show them benefits over the quick development of python/php/Javascript other than bugs in edge cases being less frequent. Don't just bemoan how unenlightened everyone is.
- nightski 9y ago
  While it is true a full formal proof of a C++ program, for example can take significantly longer and cost obscene amounts of money, that is not true when starting with this approach from the ground up. There is also a certain level of compromise. By relaxing the requirements a tad, you can still gain many of the benefits while maintaining the light and nimble feel. So why don't startups use this? Well because there are entrenched technologies that make it very difficult that have nothing to do with the merits of the approach itself. It is up to us, as developers to take the charge and push for these techniques through open source development, advocacy, and training. But to claim these techniques are a failure simply because startups aren't using them is pretty ridiculous.
  - noir_lord 9y ago
    Higher assurance from the start requires something functionally similar to Ada's Spark. I've never seen that used in the wild (though I'm in the wrong domain (web) these days).
- cube2222 9y ago
  Well, all the naysayers could also do some research instead of being as dismissive as they are. Here's an example of actual use of formal methods: http://lamport.azurewebsites.net/tla/amazon.html http://lamport.azurewebsites.net/tla/amazon.html Why aren't they used more widely? Because when people hear"math", they immediately think of it as academic. It would also be overkill for most projects.
  - dm3 9y ago
    TLA is one of the systems that are actually very practical. You can go up or down as many abstraction layers as you need . There's a great introduction written by @pron on his blog [1]. However, it's worth pointing out that you don't magically get the final program out of the TLA proof. The proof only works for the abstraction level that you chose to write it at. [1] https://pron.github.io/ https://pron.github.io/
dieterrams 9y ago
>>Writing software is not math. > You're wrong, and I've explained this upthread. I suspect there is a difference in semantics, here. Software is inherently mathematical, yes. But the practice of writing software is not the practice of doing math. The output of doing math is proofs. The output of writing software is...something that does something when run on a computer, hopefully interesting, meaningful, useful, or entertaining. In the vast majority of cases, we have not and will not need formal proofs of correctness for software to achieve these things. If I want a blur effect on some portion of a UI, and choose to implement that with a Gaussian blur, what value is there in formally proving that a specifically Gaussian blur has been applied? All of this is inherently mathematical, but that doesn't imply a need for mathematical proof.
- TeMPOraL 9y ago
  I agree. It's kind of a focus thing. When I'm writing code, I do it because I want stuff to happen - in real life, in our physical reality. Any concept of code-as-a-proof is not even on my radar, unless I'd be writing life-critical software for NASA or a hospital, or something. Here I also thing that 'Turing_Machine is both wrong in details and correct in the general point with their recipe example: > Examining the measurements, timing, and the production chain doesn't tell you anything about whether the recipe is delicious or inedible. You could, in principle, apply the knowledge of medicine, chemistry and biology, coupled with process engineering and wide-scale people studies, to construct a theory of tasty foods, which could lead to the situation in which you could evaluate any recipe on a theoretical basis. But getting to that state would require tons of up-front work to be done (some of which is being done for unrelated reasons, so maybe in the future a "food theory" will assemble itself) - and in the meantime, getting a piece of tasty food is done much faster and cheaper by finding the solution instead of deriving it. This search is done through iteration. Similarly, in software, 99% of the time we find a solution, not derive it from first principles - because the former is much cheaper when we care about the solution, and not solving the entire general class of a problem at the same time.
  - edejong 9y ago
    The same is true for math. It is the same thing, because of the Curry-Howard isomorphism. The reason for all the confusion is that programmers are already doing math. They just don't realize it and reinvent the wheels invented by the math community in the past century. It's a matter of semiotics.
didibus 9y ago
What is there to prove in most cases though? I spend half my time redefining requirements. I like Idris, and there's room for these languages. I think you give them too much credit though, programs written in them still have bugs. Your spec can be wrong. But above all else, they can't help you with scale, performance, recovering from hardware faults, and delivering what users wants. The languages are still new, they'll gain traction, and for certain use cases they'll make sense, for others they won't.
- edejong 9y ago
  The reason to use formal systems is to be able to reason about larger, more complex systems. Our brain is rather limited and to empower ourselves, we've found the divide and conquer approach. For that to work, we need assurances that our composition is correct due to the subcomponents being correct (and the composition operator). This is something we do all the time. You assume your compiler is correct, or your common libraries. However, if we want to grow larger systems, our foundations become more critical and we need stronger assurances.
jmull 9y ago
Surely you can see the part about recipes was an analogy to make a point and not directly equating two? I think you're dismissing the post without engaging its arguments, so it hardly seems fair to start calling people naive, anti-intellectual, and ignorant. (btw, we all get that these are different ways of calling someone stupid, which is never productive and isn't justified in this case.) To attempt to engage your argument, as far as I understand it... i think type systems and programming paragidms, however formal, can at best solve problems only in a corner of the problem set of software development. The limitation is because these do not take into account various kinds of constraints on software systems which nevertheless exist and are often the dominant constraints, depending on the project... Requirements, maintainability, usability, estimation, etc -- most of the stuff above the red line from the article.
jmull 9y ago
Surely you can see the part about recipes was an analogy to make a point and not directly equating two? I think you're dismissing the post without engaging its arguments, so it hardly seems fair to start calling people naive, anti-intellectual, and ignorant. (btw, we all get that these are different ways of calling someone stupid, which is never productive and isn't justified in this case.) To attempt to engage your argument, as far as I understand it... i think type systems and programming paragidms, however formal, can at best solve problems only in a corner of the problem set of software development. The limitation is because these do not take into account various kinds of constraints on software systems which nevertheless exist and are often the dominant constraints, depending on the project... Requirements, maintainability, usability, estimation, etc -- most of the stuff above the red line from the article.
scott_s 9y ago
I don't consider myself anti-intellectual, and I wrote a blog post on my claim that computer science is not math: http://www.scott-a-s.com/cs-is-not-math/ http://www.scott-a-s.com/cs-is-not-math/ We discussed it a few years ago: https://news.ycombinator.com/item?id=3928276 https://news.ycombinator.com/item?id=3928276
Turing_Machine 9y ago
> You're wrong, and I've explained this upthread. No. I'm not. Are formal math and engineering useful in cooking food? Yes, they can be (particularly if executing on an industrial scale). Are they necessary? Not really. Plenty of great cooks just throw in ingredients in the amounts that seem right to them, perhaps tasting the result once in a while. Are they sufficient? Nope. If the best mathematician and best engineer in the world collaborated, the result might be edible or it might be an inedible mess. If neither formal math and engineering are necessary nor sufficient to produce good cooking, we can safely conclude that cooking is not math or engineering. > Static type systems are arguably a product of this, especially advanced ones like Haskell's. Haskell is used by, to a first approximation, no one. Which was my point. > Now you're just being anti-intellectual. No, I'm not. > The only question is what you choose to do about that: learn the math, or stay ignorant. I was one math class away from getting a dual BS in math and CS in undergrad. Rather than stick around for another semester, I took the BSCS and went to grad school. You can safely assume that I "learned the math", and that I am not "anti-intellectual". The point here is that while, on the most fundamental level, the universe may indeed be made of math, that doesn't mean that treating everything with the math toolbox is the best way to proceed. Expecting that math methods will produce great software is a fundamentally goofy idea -- just as it would be to expect math to produce great poetry, painting, architecture, or anything else (and the same for engineering).
- jolux 9y ago
  >If neither formal math and engineering are necessary nor sufficient to produce good cooking, we can safely conclude that cooking is not math or engineering. Bingo. Good thing we're talking about programming, and not cooking. I asked if you understood what you were saying because you can't really cook declaratively, recipes are inherently imperative. The comparison to programming thus only fits for imperative languages. >Haskell is used by, to a first approximation, no one. Which was my point. If that's your point, then I agree. Not sure how that's in disagreement with my points though. >No, I'm not. So what then were you intending to convey by vague references to incomprehensible academia? Surely you weren't meaning to imply they're just wrong, were you? >The point here is that while, on the most fundamental level, the universe may indeed be made of math, that doesn't mean that treating everything with the math toolbox is the best way to proceed. Yes, but such a general claim is not what I'm arguing for. >Expecting that math methods will produce great software is a fundamentally goofy idea -- just as it would be to expect math to produce great poetry, painting, architecture, or anything else (and the same for engineering). Well, it of course depends on what you mean by "great" software. But I still think you're missing the point here. Computer science is a lot closer to math than poetry, painting, and architecture are. There is a direct, elegant, simple, formal correspondence between programs and proofs. The same cannot be said for those other disciplines. My only claim is that proofs are slightly more solid intellectually and formally speaking than programs, so converting more programs into proofs will make easier to reason about, and since programs can be easily converted into proofs (relative to poems or architecture or paintings or whatever) that this is probably a good idea. I still don't understand what your objection to that claim is.
AnimalMuppet 9y ago
The Curry-Howard correspondence says that a program is the same as a proof. A proof of what, though? Not that the program does what it's supposed to. No matter how far you go with formal methods, what the program is supposed to do is always informally specified. (There may be a formal specification. That specification wasn't handed down from on high at Mount Sinai, though. It's a formalization of the informal, badly-stated, half-unconscious informal specification that is the impetus for creating the program. Does the formal spec match the informal one? Can you prove it? No, you can't - certainly not formally. It's like you read the article, and set about disproving it, without ever really understanding it.

by jolux 9y ago

hueving 9y ago

Your post contains a lot of unnecessary aggression. Rather than suggesting someone "doesn't know what they're talking about", just provide evidence to the contrary. That aside, there seems to be something missing in your analysis, or there would be a lot of successful startups stealing the market using proof assistants and formal techniques. It's not anti intellectual to point out that programmers don't want to use academic languages that have poor usability, steep learning curves, and garbage for standard libraries. Consider when a regular house is being built. There are many problems that could be avoided if an engineering firm spent an entire year analyzing the designs and their interactions with the target site. However, that's not done because it takes significantly longer and costs obscene amounts of money. It's easier for the construction crew to fix problems as they encounter them and for the owner to do repairs on the house 40 years later. Yeah, the house isn't as reliable, but it cost 100,000 instead of 1,000,000. If you want developers and managers on your side, you need to show them benefits over the quick development of python/php/Javascript other than bugs in edge cases being less frequent. Don't just bemoan how unenlightened everyone is.

nightski 9y ago
While it is true a full formal proof of a C++ program, for example can take significantly longer and cost obscene amounts of money, that is not true when starting with this approach from the ground up. There is also a certain level of compromise. By relaxing the requirements a tad, you can still gain many of the benefits while maintaining the light and nimble feel. So why don't startups use this? Well because there are entrenched technologies that make it very difficult that have nothing to do with the merits of the approach itself. It is up to us, as developers to take the charge and push for these techniques through open source development, advocacy, and training. But to claim these techniques are a failure simply because startups aren't using them is pretty ridiculous.
- noir_lord 9y ago
  Higher assurance from the start requires something functionally similar to Ada's Spark. I've never seen that used in the wild (though I'm in the wrong domain (web) these days).
cube2222 9y ago
Well, all the naysayers could also do some research instead of being as dismissive as they are. Here's an example of actual use of formal methods: http://lamport.azurewebsites.net/tla/amazon.html http://lamport.azurewebsites.net/tla/amazon.html Why aren't they used more widely? Because when people hear"math", they immediately think of it as academic. It would also be overkill for most projects.
- dm3 9y ago
  TLA is one of the systems that are actually very practical. You can go up or down as many abstraction layers as you need . There's a great introduction written by @pron on his blog [1]. However, it's worth pointing out that you don't magically get the final program out of the TLA proof. The proof only works for the abstraction level that you chose to write it at. [1] https://pron.github.io/ https://pron.github.io/

dieterrams 9y ago

>>Writing software is not math. > You're wrong, and I've explained this upthread. I suspect there is a difference in semantics, here. Software is inherently mathematical, yes. But the practice of writing software is not the practice of doing math. The output of doing math is proofs. The output of writing software is...something that does something when run on a computer, hopefully interesting, meaningful, useful, or entertaining. In the vast majority of cases, we have not and will not need formal proofs of correctness for software to achieve these things. If I want a blur effect on some portion of a UI, and choose to implement that with a Gaussian blur, what value is there in formally proving that a specifically Gaussian blur has been applied? All of this is inherently mathematical, but that doesn't imply a need for mathematical proof.

TeMPOraL 9y ago
I agree. It's kind of a focus thing. When I'm writing code, I do it because I want stuff to happen - in real life, in our physical reality. Any concept of code-as-a-proof is not even on my radar, unless I'd be writing life-critical software for NASA or a hospital, or something. Here I also thing that 'Turing_Machine is both wrong in details and correct in the general point with their recipe example: > Examining the measurements, timing, and the production chain doesn't tell you anything about whether the recipe is delicious or inedible. You could, in principle, apply the knowledge of medicine, chemistry and biology, coupled with process engineering and wide-scale people studies, to construct a theory of tasty foods, which could lead to the situation in which you could evaluate any recipe on a theoretical basis. But getting to that state would require tons of up-front work to be done (some of which is being done for unrelated reasons, so maybe in the future a "food theory" will assemble itself) - and in the meantime, getting a piece of tasty food is done much faster and cheaper by finding the solution instead of deriving it. This search is done through iteration. Similarly, in software, 99% of the time we find a solution, not derive it from first principles - because the former is much cheaper when we care about the solution, and not solving the entire general class of a problem at the same time.
- edejong 9y ago
  The same is true for math. It is the same thing, because of the Curry-Howard isomorphism. The reason for all the confusion is that programmers are already doing math. They just don't realize it and reinvent the wheels invented by the math community in the past century. It's a matter of semiotics.

didibus 9y ago

What is there to prove in most cases though? I spend half my time redefining requirements. I like Idris, and there's room for these languages. I think you give them too much credit though, programs written in them still have bugs. Your spec can be wrong. But above all else, they can't help you with scale, performance, recovering from hardware faults, and delivering what users wants. The languages are still new, they'll gain traction, and for certain use cases they'll make sense, for others they won't.

edejong 9y ago
The reason to use formal systems is to be able to reason about larger, more complex systems. Our brain is rather limited and to empower ourselves, we've found the divide and conquer approach. For that to work, we need assurances that our composition is correct due to the subcomponents being correct (and the composition operator). This is something we do all the time. You assume your compiler is correct, or your common libraries. However, if we want to grow larger systems, our foundations become more critical and we need stronger assurances.

jmull 9y ago

Surely you can see the part about recipes was an analogy to make a point and not directly equating two? I think you're dismissing the post without engaging its arguments, so it hardly seems fair to start calling people naive, anti-intellectual, and ignorant. (btw, we all get that these are different ways of calling someone stupid, which is never productive and isn't justified in this case.) To attempt to engage your argument, as far as I understand it... i think type systems and programming paragidms, however formal, can at best solve problems only in a corner of the problem set of software development. The limitation is because these do not take into account various kinds of constraints on software systems which nevertheless exist and are often the dominant constraints, depending on the project... Requirements, maintainability, usability, estimation, etc -- most of the stuff above the red line from the article.

jmull 9y ago

scott_s 9y ago

I don't consider myself anti-intellectual, and I wrote a blog post on my claim that computer science is not math: http://www.scott-a-s.com/cs-is-not-math/ http://www.scott-a-s.com/cs-is-not-math/ We discussed it a few years ago: https://news.ycombinator.com/item?id=3928276 https://news.ycombinator.com/item?id=3928276

Turing_Machine 9y ago

> You're wrong, and I've explained this upthread. No. I'm not. Are formal math and engineering useful in cooking food? Yes, they can be (particularly if executing on an industrial scale). Are they necessary? Not really. Plenty of great cooks just throw in ingredients in the amounts that seem right to them, perhaps tasting the result once in a while. Are they sufficient? Nope. If the best mathematician and best engineer in the world collaborated, the result might be edible or it might be an inedible mess. If neither formal math and engineering are necessary nor sufficient to produce good cooking, we can safely conclude that cooking is not math or engineering. > Static type systems are arguably a product of this, especially advanced ones like Haskell's. Haskell is used by, to a first approximation, no one. Which was my point. > Now you're just being anti-intellectual. No, I'm not. > The only question is what you choose to do about that: learn the math, or stay ignorant. I was one math class away from getting a dual BS in math and CS in undergrad. Rather than stick around for another semester, I took the BSCS and went to grad school. You can safely assume that I "learned the math", and that I am not "anti-intellectual". The point here is that while, on the most fundamental level, the universe may indeed be made of math, that doesn't mean that treating everything with the math toolbox is the best way to proceed. Expecting that math methods will produce great software is a fundamentally goofy idea -- just as it would be to expect math to produce great poetry, painting, architecture, or anything else (and the same for engineering).

jolux 9y ago
>If neither formal math and engineering are necessary nor sufficient to produce good cooking, we can safely conclude that cooking is not math or engineering. Bingo. Good thing we're talking about programming, and not cooking. I asked if you understood what you were saying because you can't really cook declaratively, recipes are inherently imperative. The comparison to programming thus only fits for imperative languages. >Haskell is used by, to a first approximation, no one. Which was my point. If that's your point, then I agree. Not sure how that's in disagreement with my points though. >No, I'm not. So what then were you intending to convey by vague references to incomprehensible academia? Surely you weren't meaning to imply they're just wrong, were you? >The point here is that while, on the most fundamental level, the universe may indeed be made of math, that doesn't mean that treating everything with the math toolbox is the best way to proceed. Yes, but such a general claim is not what I'm arguing for. >Expecting that math methods will produce great software is a fundamentally goofy idea -- just as it would be to expect math to produce great poetry, painting, architecture, or anything else (and the same for engineering). Well, it of course depends on what you mean by "great" software. But I still think you're missing the point here. Computer science is a lot closer to math than poetry, painting, and architecture are. There is a direct, elegant, simple, formal correspondence between programs and proofs. The same cannot be said for those other disciplines. My only claim is that proofs are slightly more solid intellectually and formally speaking than programs, so converting more programs into proofs will make easier to reason about, and since programs can be easily converted into proofs (relative to poems or architecture or paintings or whatever) that this is probably a good idea. I still don't understand what your objection to that claim is.

AnimalMuppet 9y ago

The Curry-Howard correspondence says that a program is the same as a proof. A proof of what, though? Not that the program does what it's supposed to. No matter how far you go with formal methods, what the program is supposed to do is always informally specified. (There may be a formal specification. That specification wasn't handed down from on high at Mount Sinai, though. It's a formalization of the informal, badly-stated, half-unconscious informal specification that is the impetus for creating the program. Does the formal spec match the informal one? Can you prove it? No, you can't - certainly not formally. It's like you read the article, and set about disproving it, without ever really understanding it.