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.
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...
> If that's your point, then I agree.
You are agreeing to something that is false. See my reply to the grandparent.
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:
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.
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).