Hercuros

8 ms·

31.
by Hercuros 5y ago
I don't really think it simplifies things to change every single meeting/appointment/agreed-upon time an hour forward/backward two times a year without changing the actual clock time. If I have a weekly appointment at 11
32.
by Hercuros 5y ago
This looks pretty interesting, and it's also cool to see situations where the hardware manual says you should not do something, while in practice it is okay due to the way the hardware is actually implemented (basically, relying on und
33.
by Hercuros 5y ago
There are still some points in your explanation of data races that are not entirely correct (partly a matter of definitions). A data race occurs when two memory accesses race, and at least one of them is a write. In C/C++, data races u
34.
by Hercuros 5y ago
Speaking as someone with experience with many of those things (PL theory/formal verification background), I don't think they're even close to being a silver bullet. Coming up with the right abstractions and the right domain m
35.
by Hercuros 5y ago
Another option instead of using Rc/Arc is to use integer indices/handles into (e.g.) a vector holding your objects. Then you can have safety (in the sense of there being no language-level UB) by bounds checking your indices (you c
36.
by Hercuros 5y ago
I sometimes wonder what is the fundamental distinction between a callback-based API and this wakeup-based task API. I guess the main difference is that in a callback you generally provide the result as an argument whereas with a wakeup-base
37.
by Hercuros 5y ago
It's an interesting thought experiment IMO and you can't really resolve moral questions by looking at what the law says. After all, the law tends to be based on some moral principles, and laws can fail or be ineffective/corru
38.
by Hercuros 5y ago
Having "unsafe" mean "can wreak havoc if used incorrectly" is fine, as long as it's clear what constitutes incorrect usage, and what the behavior of correct usages is. And it does not have to be clearly defined what
39.
by Hercuros 5y ago
Relegating parts of the memory model with unclear/hard-to-specify semantics (i.e. relaxed or consume) to the "unsafe" part of the language is an interesting idea, but it kind of goes against the spirit of "unsafe" (
40.
by Hercuros 5y ago
My point was basically that you can implement the array abstract data type (creation, set value at index, get value at index) in a lot of ways, including by using ADTs (although it seems hard to get an O(1) implementation if you use ADTs, u
41.
by Hercuros 5y ago
This is not true for classical logic, because AND can be written using NOT and OR using DeMorgan's law.
42.
by Hercuros 5y ago
Although if you just consider 1-1 correspondence, then basically any type with a countable number of inhabitants is isomorphic to the integers (when the type is viewed as a set of inhabitants). And that makes sense, because we can always ju
43.
by Hercuros 5y ago
Wouldn't the compiler be allowed to elide the memory accesses that are being used to poke the memory region? If you are doing the poking before the memory has been initialized, then I'm not sure there are any guarantees that the c
44.
by Hercuros 5y ago
You can have UI workflows just as well with a language that has (runtime-managed) green threads, like Go and Elixir. It's just that you sometimes have to make sure that certain green threads have their actions scheduled on the UI (OS)
45.
by Hercuros 5y ago
It's also important to realize that the standard Turing machine doesn't actually have an infinite tape, but rather it has a tape that can grow to hold an arbitrarily long, but still finite, sequence. At any point during the execut
46.
by Hercuros 5y ago
> I've had a professor like that and it takes a while to realize that those people are needed. For lazy students it may be a proper wake up call to the real world Though it should be mentioned that just as frequently (if not more) s
47.
by Hercuros 5y ago
I think it is still understandable though that making those kinds of technical corrections about a study could be perceived as "defining away the problem" or getting too technical about a (potentially) real societal issue. The mer
48.
by Hercuros 6y ago
Note that Kevin Buzzard is talking in the context of convincing "mainstream" mathematicians to use a proof assistant. He specifically clarifies somewhere (not sure where in this video, but I've seen other videos where he clar
49.
by Hercuros 6y ago
To be fair, you don't hear (as much) about all the Mark Zuckerbergs who weren't quite so successful. If you're going to look at some of the richest people on the planet, then of course you'll see a string of successes, b
50.
by Hercuros 6y ago
If you can afford a garbage collector, then you can also just use something like Haskell or OCaml or Python, which also gets you memory safety. No need to think about lifetimes or different types of smart pointers. Not saying that it’s a lo
51.
by Hercuros 6y ago
What does it mean for a type system to be “complete”? Type soundness means that well-typed programs do not “get stuck”, but it is not obvious at all (at least to me) what it means for a type system to be complete, formally speaking. If you
52.
by Hercuros 6y ago
I think that just because most people do not write compilers for a living does not mean that it’s not useful to have implemented one. Writing a toy compiler properly is an interesting programming exercise that involves steps such as parsing
53.
by Hercuros 7y ago
I never really understood the point of view that depressed people somehow are more realistic, seeing things as they “really are”, while non-depressed people are overly optimistic. Maybe it’s true in the limited setting of a study, but depre
54.
by Hercuros 7y ago
I don’t think they are going to be phased out, since including lifetime specifiers is a means of documenting intent (they are part of a function’s public interface). Removing them would mean that seemingly irrelevant internal changes to fun
55.
by Hercuros 7y ago
That's a fair point. I do think that we essentially live in a world that is built up largely out of psychological/social constructs and mental abstractions. In a lot of ways, a psychological or social construct can be a lot more &
56.
by Hercuros 7y ago
> This might all sound pretty dark, but the good news is that nothing you do is really important. The universe will remain unperturbed no matter what actions you take (or don't)! So if you're stressing about how well you live,
57.
by Hercuros 7y ago
Mixed integer programming is a more specialized task than SMT solving, therefore an MIP implementation is likely to be more optimized for the task, even if you might be able to use an SMT solver to solve the same problem. Moreover, SMT solv
58.
by Hercuros 7y ago
Dependent types are not just useful for proving correctness properties, and in fact I think dependent types in Haskell are not really intended to prove really complex properties, like the full functional correctness of a compiler. Hence, I
59.
by Hercuros 7y ago
People are saying that you do not just submit your trained model to Kaggle. You also submit the code that was used to train the model from the training set, which is used in the winning models to train them from scratch on the training set.
60.
by Hercuros 7y ago
It should also be mentioned that general statements or studies about the relative mathematical or technical abilities of men and women do not necessarily have any direct bearing on specific groups of men and women, like “people who have suc

More ›