Hercuros

11 ms·

61.
by Hercuros 7y ago
I think the answer to this is not to start having general feelings of doubt about generally accepted conclusions in science. Rather, we need to be much more specific about where we think that groupthink is playing a role, looking at things
62.
by Hercuros 7y ago
Things are of course not so black-and-white. It is hard to discuss these things at a general or abstract level, since things are often different in practice than they are in theory. But my point was to show that there are actual reasonable
63.
by Hercuros 7y ago
I think your point about disingenuous arguments made by static typing proponents is mostly reasonable, but I don’t think those are the only arguments to be made for strong static typing. Other benefits of strong static type systems are comp
64.
by Hercuros 7y ago
I think it is a bit of an oversimplification to say that Haskell is less popular because it is not as easy to "copy/paste" together code for it. I would say it also isn't that easy to copy/paste together C++ code, f
65.
by Hercuros 7y ago
Haskell is significantly less popular than some other languages, but it has a non-trivial amount of people using it in serious applications in industry (e.g., a large part of Facebook’s spam filtering system is written in Haskell [1]), as w
66.
by Hercuros 7y ago
I just occasionally clear videos from my Watch History which I do not want to be used for recommendations. It’s become a habit to do this every once in a while, and doesn’t take a lot of time.
67.
by Hercuros 7y ago
No, because the concentration is a big part of the problem. If things were more spread out, but with the same total amount of nitrogen, there would be less of an issue (and this is why Germany has less strict rules on nitrogen).
68.
by Hercuros 7y ago
Moving the production to a different country would be a solution, since the Netherlands is currently producing way more nitrogen per area of land than other European countries. Moreover, our nature areas are generally smaller and closer t
69.
by Hercuros 7y ago
Programming is in my opinion not just about data structures and algorithms. It is also about designing abstractions that capture the domain you're working in well, whether it be by designing classes in an OOP language, or data types an
70.
by Hercuros 7y ago
It's unnecessary to set a fine so high that the person doing it would "pay back" the harm to society on average if they did it. You merely have to set a fine so high that it deters people from doing it. Let's say speedin
71.
by Hercuros 7y ago
Yes, strictly speaking that's true, but then if the universe were slightly bigger, or you used a different encoding, you'd get different results. It feels kind of arbitrary to stop thinking about what would happen if the universe
72.
by Hercuros 7y ago
Diagonalization arguments (which are used in Gödel's theorem) do require some infinity. If there were only a finite number of such "True, but unprovable using your current proof rules" sentences, then you could simply add tho
73.
by Hercuros 7y ago
Infinity is the only reason: all finite sets of strings are decidable, simply because you can just keep a list and see if a string is in there. Important to mention that there are decidable infinite sets of strings. For instance, deciding w
74.
by Hercuros 7y ago
It’s mostly a matter of practice. I think that many people’s experience of functional programming is a (potentially poorly-taught) university course, during which there is not really enough time to really become comfortable with functional
75.
by Hercuros 7y ago
Is this view of FP based on actual experience maintaining a non-trivial program written in an FP language? In my experience, FP doesn’t necessarily add a lot of unnecessary complexity. Sure, languages like Haskell are perhaps initially a bi
76.
by Hercuros 7y ago
You could indeed make the case that the intractability/undecidability-type theorems suggest that the problem of program verification is inherently difficult, and not something that can be solved in most cases using a trick. It requires
77.
by Hercuros 7y ago
What I meant by non-sequitur is that I agree with your premises (that certain problems are computationally intractable or undecidable, and this is good to know), and I agree with your conclusion (full verification using deductive methods&#x
78.
by Hercuros 7y ago
I agree that verifying programs using dependent types is impractical for large programs. I think that the reasons are mostly practical rather than theoretical, however. There's too little benefit for too great a cost if you want essent
79.
by Hercuros 7y ago
I also mentioned this in my other post, but the CompCert compiler is a highly non-trivial example of a program verified using dependent types, and which would not really be possible using automated methods. Of course, not very affordable, s
80.
by Hercuros 7y ago
First of all, I would agree with you that full formalization of program correctness using dependent types is generally extremely costly in terms of time and money, and that there are often other formal methods which might get you results th
81.
by Hercuros 7y ago
This paper is almost entirely incomprehensible to me, and I have a background in formal logic. It might be that there is some error in the proofs that this author is referring to, but the paper does not make any clear point about what the p
82.
by Hercuros 7y ago
I think that for function definitions in Rust you would in principle be able to leave out lifetime annotations on arguments/return values in more cases than is currently allowed by lifetime elision. I believe they don't allow this
83.
by Hercuros 7y ago
I think there are essentially two ways of making the compiler statically aware of lifetimes: you can annotate the program with lifetimes, as in Rust, or you can have the compiler infer all of the lifetime information somehow. Adding annotat