Kutta

9 ms·

31.
by Kutta 7y ago
As a mid-level Chernobyl geek, I found this show generally underwhelming. I admit it may hold much more interest for those who are not yet familiar with the story. But I must say, there are so many things which could have been done spectacu
32.
by Kutta 7y ago
You can only see LEO satellites near dawn and dusk. They are in shadow most of the time at night.
33.
by Kutta 7y ago
Agreed. Conjunction fallacy galore in parent post.
34.
by Kutta 8y ago
You mean algebraic effects? Monad transformers are an effect system as well.
35.
by Kutta 8y ago
That's irrelevant, all mainstream proof assistants are compatible with classical logic.
36.
by Kutta 8y ago
Wrong. Division is not part of the field axioms, it is a defined function, and changing its definition has absolutely no bearing on the consistency of your equational theory.
37.
by Kutta 8y ago
> no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected This is an unfortunate glaring false statement in the Morte documentation. Correctness of refactoring and code abstracti
38.
by Kutta 9y ago
Not wanting to learn a different language is a justifiable preference. Software is full of cost/benefit questions like that. Believing true things also doesn't make you uncharitable.
39.
by Kutta 9y ago
> is it impossible for a criminal to be a hero? I think this is an awful question with awful answers. http://squid314.livejournal.com/323694.html
40.
by Kutta 9y ago
> small portion of the radioactivity escaping the containment shell The Chernobyl reactor was very unsafe by modern standards, it did not have a containment vessel and tens of tons of reactor material was blown into the air, not a small
41.
by Kutta 9y ago
> The more expressive a type system is, the more difficult type inference becomes. This is always mentioned and I always fail to see the relevance. Inferable terms stay inferable when we add dependent types.
42.
by Kutta 9y ago
Unfortunately, beta-eta reduction on Church-coded terms (as in Morte) is much weaker than what is commonly understood as supercompilation, and it is false that "no matter how many layers of indirection you might add the binary size and
43.
by Kutta 9y ago
The society can't ever be honest and collectively stop enabling whatever. Everyone all the time responds to incentives, and power goes to whoever is lucky and good at collecting votes and support. Competence, technological acumen or vi
44.
by Kutta 9y ago
I am familiar with all of your listed sources (even attended one incarnation of the Érdi Gergő talk). Section 3.2 of the paper absolutely does not say that the result does not hold. The main point of the construction is that typed quoted re
45.
by Kutta 9y ago
f :: String -> () f g' = case (eval g' :: Maybe (String -> ())) of Just g -> g g' Nothing -> () loop :: () loop = f (quote f)
46.
by Kutta 9y ago
Previous discussion on /r/haskell: https://www.reddit.com/r/haskell/comments/3s93w1/a_selfinter... To summarize, there are a number of different notions of self-interpretation. The strongest no
47.
by Kutta 9y ago
You know about the word "evidence"?
48.
by Kutta 10y ago
I've seen this over and over but it's false. Adding dependent types do not negatively affect type inference for the non-dependent fragment in any shape or form. On the contrary, Agda/Coq type inference is far more powerful th
49.
by Kutta 10y ago
Obviously, we should not compare small personal project languages with decades-old industry languages by factors determined by the sheer amount of work thrown in. We compare them mostly by fundamental design principles. In this case, partia
50.
by Kutta 10y ago
The same thing as far as I see.
51.
by Kutta 10y ago
I'm fine with classical reasoning and uncomputability, and I acknowledge the intuition for classical truth (it got popular for a reason). But pretty much all the useful classical math can be performed all the same in type theory withou
52.
by Kutta 10y ago
HoTT doesn't build on any notion of omega groupoids; at the lowest level it's a collection of typing and computation rules which one can apply successively to do proofs and constructions. The resulting constructions can be interpr
53.
by Kutta 10y ago
Evaluation is always implicitly used in any sort of mathematical formalism. "2 + 2" is a program which evaluates to "4". Type theory just makes the computation arising from substituting definitions rigorous. Not letting
54.
by Kutta 10y ago
My perspective is that classical axiomatic theories have a far weaker philosophical grounding than constructive type theories. In type theory every definable natural number is a program which evaluates to a concrete finite numeral. You can&
55.
by Kutta 10y ago
malloc and free are indeed far more expensive than allocation in a runtime system with copying GC.
56.
by Kutta 10y ago
Yes. Copying GC with bump pointer allocation is critical for pretty much any persistent data structure. In C++ and Rust one should use memory pools/arenas for them instead.
57.
by Kutta 10y ago
Musk doesn't primarily raise capital by selling prospects of eventual dividend. He openly doesn't care at all about profitability, he only cares about the oft-stated SpaceX/Tesla goals, and is pretty much willing to take any
58.
by Kutta 10y ago
You have given a fairly comprehensive explanation (here and in other comments) as to why it's unreasonable to be disturbed by the chanting and why it would be beneficial for SpaceX employees to be let chanting as they wish. I don'
59.
by Kutta 10y ago
Pascal's wager's application to real-world cost-benefit calculations is pretty much always a fallacy: http://lesswrong.com/lw/z0/the_pascals_wager_fallacy_fallacy... Large payoff and small chance (with a
60.
by Kutta 10y ago
If cryonics suddenly worked, we'd need to face the extremely serious question of why we let almost everyone die before, i. e. how we could've made one of the most catastrophic humanitarian and public health oversights ever.

More ›