Comment by Turing_Machine | Hacker News Reader

Comment by Turing_Machine | Hacker News Reader

Parent Full thread

>I think it's self-evident that there is no theoretical basis for software development in the way that would satisfy your criteria.

Yes. Writing software is not math. Does it use math concepts? Of course, but so does just about everything else. While we're at it, writing software is also not engineering, even though there are engineering concepts that can be applied.

Writing software is its own thing. Pretending that it's something else (like math or engineering) invariably leads to category errors.

Think about food recipes. They certainly use measurements and timing, and engineering principles can certainly be applied (especially when executing them on an industrial scale) but they are not math (or engineering) either. Examining the measurements, timing, and the production chain doesn't tell you anything about whether the recipe is delicious or inedible.

Arguing that a piece of software should be "proven correct" makes about as much sense as arguing that a recipe should be "proven correct". You might as well judge the recipe by the standards of poetry ("Does it have evocative imagery? Does it rhyme or alliterate well?").

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). 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). Alternatively, the "programming is engineering" people come up with some baroque formal process that requires you to write a 500 page document and get six committees to sign off on it before you can write "Hello, world". I'm old enough that I've seen these things happen multiple times.

>It's also self-evident that in most situations, correctness and reliability aren't a concern.

I wouldn't say they aren't a concern at all, but if you're wasting six months screwing around with formal proofs, UML diagrams, or things of that nature, while in the meantime your competitor is iterating three or four times, that is definitely a concern. Operate that way and your milkshake is going to be drunk, yo.

>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.

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.

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.

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).

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 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.

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/

>>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.

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.

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.

Nah, I still think it's about different goals.

But assuming you're right, I'd like to know - what mathematical wheels am I reinventing in my dayjob of building UIs that let people click up some stuff that later gets put in business-specific XMLs?

You're defining relationships between types through functions.

Math, at least applied math, is not the goal, but the method. Programming neither is the goal, it is the method. Understanding that both are language to express the path is of the essence.

The XML as a vessel of human-knowledge is limited. Good intentions have brought it OWL/RDF, XML Schema, XSLT; examples where others before us have tried to extend the XML into the domain of semantics and algorithms. Nevertheless, it was found that, without an expressive type system, large and complex business domains cannot be modeled. Apparently, in order to model abstract business domains, we need a language that composes both high- and low-level with near invisible seams.

So, that click-your-XML-application might benefit from a reflective logic, enabling the user to explore the possible state-spaces. If your app uses relational algebra from DBMSs, it might be able to combine the relational algebra with the algebra defined by your schema's. The UI state-space and the XML schema might be an isomorphism, which helps prove completeness of your UI-builder implementation.

Above all, the mathematical way of thinking helps reasoning, communication and correctness. It might not be the only way or perhaps the way is dated. Nevertheless, ignoring math as a programmer, feels like ignoring music theory as a musician or linear algebra as a structural engineer.

We haven't been arguing that programming can't benefit from math.

> ignoring math as a programmer, feels like ignoring music theory as a musician or linear algebra as a structural engineer.

We're not ignoring math.

Curry-Howard isomorphism does not mean the same practices that are performed in mathematics research must be applied to writing software.

Some aspects of language design are reinventing wheels invented by the math community. This is far from constituting the set of "writing software" or "software engineering".

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.

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.

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.

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/ We discussed it a few years ago: https://news.ycombinator.com/item?id=3928276

> 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).

>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.

>>Haskell is used by, to a first approximation, no one. Which was my point.

> If that's your point, then I agree.

You are agreeing to something that is false. See my reply to the grandparent.

> The comparison to programming thus only fits for imperative languages.

I am not comparing recipes directly to programming. I used recipes as an example of something that has mathy and engineery facets, but that is not engineering or math.

> So what then were you intending to convey by vague references to incomprehensible academia?

I wasn't making "vague references" to anything, nor did I say that academic languages were "incomprehensible". I did say they were bizarre, which is a different thing entirely.

I'm not sure why you find it hard to believe that someone could understand academic languages of the sort you evidently prefer, and yet somehow still choose not to use them. Your attitude seems to be that anyone who doesn't use your preferred methods is "anti-intellectual", "ignorant", or any of the various other personal insults you've used.

Why not just go off and write some awesome software using your methods? If they work as well as you claim, you'll have some hard evidence to back up your assertions

>There is a direct, elegant, simple, formal correspondence between programs and proofs."

You are defining great software as "software that can be proved to behave in accordance with some formal spec", while people who actually use software (i.e., the people who pay the bills) define great software as software that performs the task they need to have done, can be written economically, and that is easy to use.

By your definition, a great recipe would be one that came out exactly the same every time, even if it tasted like shite, or took three weeks to make, or...

> Haskell is used by, to a first approximation, no one. Which was my point.

Unless you have a very loose definition of"no one" that simply is not true.

Just off the top of my head:

Haxl at Facebook Bond at Microsoft Supply chain management at Target

Also see:

https://wiki.haskell.org/Haskell_in_industry

>Unless you have a very loose definition of"no one" that simply is not true.

What part of "to a first approximation" was unclear?

https://www.tiobe.com/tiobe-index/

Haskell is in 47th place, which is consistent with where it ranks in every other popularity list I've ever seen.

I'm standing behind "to a first approximation, nobody".

Note that I'm not saying that Haskell is a bad language, or that Haskell programmers are bad people or anything like it.

I'm saying that the vast majority of programmers do not use Haskell. An anecdote about a particular group that uses Haskell (or even several groups) does nothing to refute that fact.

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.

well that pretty much nailed it.

Reply on news.ycombinator.com