This is ridiculous. If not being able to prove everything doesn't help, we should get rid of type systems altogether. Programmers are so complacent and ignorant to what their compilers provide them out of the box, they forget how many brilliant people, proofs, and countless hours it took to create those features.
>> But going into psychology and thinking about making things easy for humans goes against what is generally accepted in CS research.
Well, no. Just because you don't understand or care to learn how much pain and work it took to get rid of seemingly arbitrary restrictions of type systems doesn't mean that it is not considered CS research. You think Rust's region types that literally prevent you from leaking memory without garbage collection came out of a hackathon? Java's generics are a usability improvement, isn't it? Do you have any idea about who designed that? Don't even get me started on any of the features in pure languages.
And even if you were so blind to reject all of these as improvements, psychology and usability of programming languages is an actual CS research field with its dedicated conferences. Here's a master's course [0] from University of Cambridge Computer Laboratory.
Remember the last couple of bug studies? They didn't show type systems having an effect on reducing number of bugs, but instead showed only significant correlation being number of LOCs. And yet dynamically typed languages require fewer lines to express the same thing.
The point of mathetic's comment was to point out that a lot of ("computer science") mathematics goes into the design of the compilers and interpreters that software engineers use every day. And that it's rather ignorant for a user of one of these modern interpreters or compilers (even of a dynamically typed language!) to claim that this math doesn't matter or isn't useful.
> Remember the last couple of bug studies?
Which studies? There have been at least half a dozen high profile empirical studies about type systems in top tier conferences in the last 5 or 6 years, and probably dozens more in journals/conferences I don't follow.
The empirical evidence is predictably mixed. E.g. Hanenberg has published papers cutting in both directions re: usefulness of type systems.
Also, there's still very little empirical evidence about many type systems. There's a lot of Java vs. X comparison papers, but very few rigorous empirical studies on Haskell or SML or OCaml or Scala, for example. And I'm not aware of a single empirical comparative study on a dependently typed language.
> They didn't show type systems having an effect on reducing number of bugs
Actually, there are empirical studies that show type systems reduce bugs.
Also, as a separate matter, your summation of the available evidence is inaccurate to the point of absurdity. There is not a single shred of empirical evidence for your unconditional claim that type systems don't have an effect on reducing bugs. That hypothesis has never experimentally tested. Furthermore, the empirical data we have suggests that hypothesis is wrong.
Science works by looking at all the evidence and coming to informed conclusions. Cherry picking the N out of M studies that confirm your priors and then generalizing their results far beyond the parameters of the actual study is the opposite of scientific thought.
> but instead showed only significant correlation being number of LOCs.. And yet dynamically typed languages require fewer lines to express the same thing.
My OCaml programs are very often far shorter than my Python programs. Again, your unconditioned claims are getting you in trouble.
You probably mean to say something like "Java programs are usually longer than Python programs", in which case you have a reasonable critique of Java's type system, but not of type systems in general -- or even of the half dozen type systems that are radically different from Java's and in wide-spread use in production environments. And in fact, most adamant supports of type systems are probably some of the most ardent critics of Java's type system, so rejections of type systems on the basis of Java comparisons are a bit of a straw man IMO.
If there's a single thing that ALL of the various empirical PL design researchers could agree on, it's that the sort of unconditioned claims that are made in your post should be avoided.
I discovered TLA+ when I needed to design a complex distributed database. I learned it in a couple of weeks, and immediately put it to good use. It quickly uncovered some (big!) mistakes in my original idea, and helped me find a solution. So my motivation to learn and use TLA+ was, like Amazon's, 100% pragmatic and not at all academic.
That's precisely what you need to do in order to have a valid proof. I'm not sure why you'd say this?
I think the point is that you can have a proof of correctness in a crypto package that doesnt account for power-usage side-channel attacks, for example.
This is true, but beside the point: a library with no proofs about it doesn't solve that problem, and the library with proofs tells me I don't have certain problems for sure.
The question is then: is it worth the proof development effort to only get those partial guarantees? I would argue yes, for a lot of reasons (and high EAL levels tend to agree that it is for high-assurance stuff), but it's a matter of some debate.
You're right that you can take a mathematical proof out of the realm of abstract math and it's new domain may not have all the guarantees we need, but this means we need to extend the system to account for the new domain (and within this domain, the proof is not valid).
But the poster doubled down on this idea that "there are constraints proofs ignore" within the existing domain. Outside of convenient proofs that upper division students provide, this is not true.
A good example of this process and the nature of "pure" CS interacting with the real world is the field of distributed databases. As the field has grown, proofs are expected to aggressively model real world conditions and in fact go further, modeling outright adversarial conditions unlikely to occur in the real world.
I was merely reiterating a common (and I think sensible) point that we can't write proofs about things we don't have the computational resources to address or just plain don't realize are an issue. Both are very real challenges to using proofs about our software, and should be kept in mind when talking about the field.
The said, Im a proponent of everything from proofs about abstract algorithm properties to basic model checking on a spec to using formal methods to extract a program with guaranteed propertied from a formal spec we've written proofs about in something like Coq.
DARPA funding HoTT research should clue anyone in that this stuff is useful.
I just see people talking about domains and saying, "We don't need proofs for software" like they learned literally nothing from OpenSSL last year. And perhaps they did not, but I think we all should recognize that the stakes are getting pretty high and it's time to stop pretending we're all supervillan-level software designers.