> Could you imagine people saying the issue with Java is its extremism towards objects and method calls?
I think exactly that all the time. It’s ridiculous.
> That's a problem no haskell user has, honestly.
I had this problem all the time when trying to write games in Haskell. Not every subject matter decomposes into semirings. Just like not everything decomposes nicely into objects.
People tried to fix this with FRP or lenses. Both are worse than imperative programming for games imo.
I’ve been working with pure functional languages and custom lisp dialects professionally my whole tenure.
You get a whole bag of problems for a very subjective upside.
Teams fragment into those that know how to work with these fringe tools and those who don’t. The projects using them that I worked on all had trouble with getting/retaining people. They also all had performance issues and had bugs like all other software. You’re not missing out on anything.
Many problems stem from people not being willing to learn another paradigm of computer programming. Of course teams will split, if some people are not willing to learn, because then some will be unable to work on certain things, while other will be able to do so.
You mention performance. However, if we look at how many Python shops there are, this can hardly be a problem. I imagine ecosystems to be a much bigger issue than performance. Many implementations of functional languages have better performance than Python anyway.
There are many reasons why a company can have issues retaining people. A shitty uninteresting product, bad management, low wages, bad culture ... Lets eliminate those and see whether they still have issues retaining devs. I suspect, that an interesting tech stack could make people stay, because it is not so easy to find a job with such a tech stack.
However, many companies want easily replaceable cogs, which FP programmers are definitely not these days. So they would rather hire low skill easily replaceable than highly skilled but more expensive workforce. They know they will not be able to retain the highly skilled, because they know their other factors are not in line for that.
Most database companies run only a small amount of tests before committing. After committing, you run tests for thousands of hours. It sucks. You probably do this all day every day. You just run the tests on whatever you have currently committed. you kind of have to be careful about not adding more tests that make it take much much longer.
See https://news.ycombinator.com/item?id=18442941
Ahh, thanks, that piece of information suddenly makes TFA makes sense. I was wondering how it could be that those issues were not caught by unit tests before committing/merging, but seemed to be caught soon afterwards in a way that they could still immediately be ascribed to a specific commit.
Yeah but second order logic itself is incomplete. ZFC doesn't have a single model, too, btw. In the end unprovable sentences exist because there are multiple models satisfying your axioms.
What I meant to say is that multiple models are not the only reason for something to be true but unprovable, the incompleteness theorem also holds in more general conditions.
Concerning multiple models of ZFC: I'm always confused by such statements about the foundations of set theory itself, they seem weirdly self-referential. ZFC certainly can't prove that it has multiple (or even any) models. Does such a statement need additional axioms, or is there a general theorem like "If a first order theory has any model, then it has multiple ones."?
"What I meant to say is that multiple models are not the only reason for something to be true but unprovable, the incompleteness theorem also holds in more general conditions." I can't give a clean rebuttal for this, but I believe this to be profoundly mistaken. It might be technically correct though, depending on how you'd formalize this statement.
To formalize math you need a logic that has some properties: it should be decidable whether a proof is correct, you should be able to write it down, it should not be contradictory. If you take these together the only way a statement is unprovable, is if it is independent from the axioms, i.e. there exist multiple models.
I see. Checking the formulation of the incompleteness theorem again, I noticed that I probably misunderstood something here: it indeed essentially requires proofs to be verifyable, which second order theories do not provide. So second order PA can (and in fact does) have a proof of every statement or its negation, without contradicting incompleteness, but provability is somewhat useless in this case. For theories that fit the conditions you listed, unprovability is indeed due to multiple models. Does that make sense?
Edit: however, consistent second order theories don't always have a model. In first order, if S is an undecideable statement in theory T, then both T+S and T+!S have models, both of which are models for T, so undecideable statements always come from multiple models. But that does not need to be the case in second order, so your claim "it is independent from the axioms, i.e. there exist multiple models" is not neccessarily true, i.e. there may be cases when decideability of some statement fails in a theory with a unique model. Or is there another argument for your claim?
Forgive me for spamming questions, I just try to understand how these things fit together. But maybe we should just stick to first order, since everything else is too weird anyway.
True, but if you add too many axioms, the resulting set of axioms will not be computable anymore. If you allow your set of axioms to not be computable you can of course just use the set of statements that are true for whatever model of the natural numbers you have in mind. The whole point is that it's not possible to write down any sensible definition of what natural numbers are supposed to be.
This is a mischaracterisation of gödels incompleteness theorem.
The set of axioms the theorem is about isn't even mentioned in the article. This is very important. If you pick the empty set as your axioms, most statements will be independent of them.
The important insight is different. One can simulate a computer in the peano axioms.
If you could prove or disprove (starting from a computable set of axioms) every statement about simulated computers you could also solve the halting problem.
Kleenes (the kleene star guy) proof goes that way.
I think exactly that all the time. It’s ridiculous.
> That's a problem no haskell user has, honestly.
I had this problem all the time when trying to write games in Haskell. Not every subject matter decomposes into semirings. Just like not everything decomposes nicely into objects. People tried to fix this with FRP or lenses. Both are worse than imperative programming for games imo.