Kutta

It will release approximately no CO2.

The "small amounts is cardioprotective" is most likely false, the new recommendation simply reflects this. I recall reading about this in research more than 10 years ago. (Sorry for not citing, I'm on mobile rn)

Yes, the point is that the user only has to write an interpreter, not a compiler, the compiler is automatically generated. See also GraalVM's Truffle interpreter or Souffle Datalog.

Futamura projection is an entirely standard concept in staged compilation. The hand-wringing is unwarranted.

I would also guess they don't give a fuck about the night sky either.

Are you literally not aware that all pieces of internet infrastructure currently in use have to be replaced every N years?

Arenas have been used in Rust for a long time.

We already have a perfectly good foundation of mathematics. It's called ZFC [1]

This is completely missing a core point of category theory and type theory (which is about categories equipped with certain extra structure), which is to work is settings which can be flexibly tightened or loosened in order to do constructions which are as general as possible. A theorem in HoTT is far more widely applicable than a theorem in ZFC; HoTT can be interpreted in any higher Gröthendieck topos, ZFC can be only intepreted in a certain class of 1-toposes. In HoTT, we can simply assume choice and LEM to internally reproduce ZFC. In ZFC, univalence is false and cannot be assumed.

It's not at all clear HoTT, or type theory in general, is the best solution for formalizing mathematics

Xena project isn't too hot on HoTT indeed, but they will tell you that type theory in general is absolutely the best solution for formalizing mathematics.

in particular denying the law of excluded middle

MLTT does not deny LEM, nor HoTT. The point is not to deny LEM, but to work in a more general system which does not necessarily assume it.

What you say is kind of interesting but I get the impression that we are talking past each other.

id(X): ==(X, rec_0(0, X))

Sorry, what's this supposed mean, is it a definition? The propositional equality type has two or three arguments, I only see one (X) here, if as you say "id" is propositional equality.

In any case, nothing peculiar happens when we check a trace-annotated proof of bottom. We are free to use any particular finite-step unfolding of the non-normalizing proof.

We also don't need any paradox or inconsistency for a non-normalizing term, it is enough to work in ETT in a typing context which implies bottom, or which contains an undecidable equational theory, e.g. the rules of the SK-calculus.

The actual proofs of decidability of type checking (e.g. from Martin-Löf‘s original paper) are conditioned on the normalization theorem

Decidability of type checking is always relative to a particular surface/raw syntax. A trace-annotated raw syntax does not need a normalization assumption for type checking.

A type system cannot be TC. What you seem to talk about, is that if a type checker can simulate arbitrary TM's through an encoding of its input, then the type checker is necessarily non-total. This is correct. But the Idris checker is total and it is not possible to use it to simulate TMs.

The Idris type system does allow you to specify and formalize TMs internally, but that has no bearing on decidability of type checking, as I explained before.

I don't see that "normalization implies consistency", which I'm aware of, relates to my previous comment in any relevant way.

ZFC and MLTT do not differ in that decidability of proof validity is not related to logical expressiveness.

It's not even true that for type theories, decidability of proof validity implies normalization. Normalization is not logically equivalent to decidable type checking.

For example, we can have a term language for extensional type theory which is annotated with reduction traces. This is the kind of syntax that we get when we embed ETT inside ITT. It has decidable type checking, as the type checker does not have to perform reduction, it only has to follow traces. This kind of tracing is actually used in the GHC Haskell compiler to some extent. So we have decidable type checking for a surface syntax of a type theory, for a type theory which is a) consistent b) not strongly normalizing.

Incorrect. Whether the language as a logic is capable of expressing undecidable statements, is orthogonal to whether type checking is decidable. Type checking is analogous to checking proof validity in logics. Commonly used proof systems for first-order or higher-orders logics admit decidable proof validity, and already many first-order theories allow expressing undecidable statements. ZFC is a rather obvious example. Likewise intensional type theory is highly expressive as a logic and admits decidable proof validity.

Decidability of type checking is instead related to how explicit surface syntax is. In intensional type theory, the usage of equality proofs is marked explicitly, which is sufficient to retain decidable type checking. In contrast, in extensional type theory, the usage of equality proofs is left implicit, which causes type checking to be undecidable.

OpenAI should have never been open, named "OpenAI", or advertised itself as being open. At the time of OpenAI's inception, much of the AI risk community deemed it as harmful, although that wasn't spoken out a lot, because it is a delicate affair to criticize misguided effort on AI safety when the status quo was almost no effort being spent on AI safety at all. It is a minor consolation that OpenAI turned out to be less open than initially advertised.

https://web.archive.org/web/20200518081726/https://slatestar...

This tutorial seems to miss the level-based generalization optimization, which is crucial for production-strength HM inference. For, that you can look at:

http://okmij.org/ftp/ML/generalization.html

I also recommend Nick Bostrom's article "The Future of Human Evolution", predating OP by ten years, which contains essentially the same arguments and conclusions.

https://www.nickbostrom.com/fut/evolution.html

Usually it's not possible to form such a predicate. If we have impredicative base universe, then it's possible to form a predicate over all types in the base universe (which may or may not be all types in the language), including the predicate itself. However, this feature is rarely used in type theory, because it is incompatible with classical logic.

In programming, this is more commonly available, because we don't necessarily care about propositions, let alone classical logical proofs. The polymorphic identity function type `forall a. a -> a` in System F quantifies over all types including itself.

The human spaceflight ability of NASA trended sharply to zero in the last 50 years, with space travel getting more expensive, more dangerous and far less capable than before, going from moon transfer to LEO only to no human spaceflight whatsoever. If you prefer to abolish human spaceflight, then you can be happy with NASA, if not, then you have to present rather strong evidence why the status quo will magically yield better outcomes.

Immutability is an implementation detail with no inherent value. What we actually care about is referential transparency, encapsulation & tracking of effects, performance, abstraction, thread/type/memory safety, etc. The State monad in Haskell is implemented without mutation, but presents an API with mutation. The ST monad is implemented with mutation but presents a pure and referentially transparent external API.

It is fair to say that functional programming is primrarily in favor of immutable data structures because it is simpler to implement them efficiently in a setting where referential transparency is the default. Mutation (meaning referential intrasparency) is just more complicated, and we need heavier machinery to structure it nicely. We may use linear/substructural types, uniqueness types, regions, etc for this purpose, but here are a number of choices, and the picture is not as clear-cut as with plain pure lambda calculi. Just remember that mutation is not bad by itself, many functional programmers are often happy to speed up production code with mutation, it's just that it is usually more complicated to structure nicely.

I thought the cost of GC following a pointer into a compact region is basically constant time, or is that incorrect?

I agree that storing a reference besides an Entry is probably safer than #touch. It's also similar to arrays slices, where we store reference to the array itself + offsets.

The ST-like region typing can be still useful though, because we get a static bound on the lifetime of a compact region. We'd prefer to avoid leaking space via large compact regions which survive beyond their intended life.

You need something which decreases on each step. You could try to recurse on the number of unvisited nodes in the graph. You can try well-founded recursion if this does not work for some reason.

Awful comment. The OP, while not pedagogically ideal, demonstrates proof writing along the Curry-Howard correspondence, an extremely deep topic which predates popular functional programming and OOP by decades. To liken this to "tool fetishization" is pure nonsense.

You can always put a project into a reference class consisting only of failed projects. You can also put this project into the class of Tesla factories, none of which failed so far.

Within EU, immediate local demand is barely relevant compared to labor and manufacturing conditions, for setting up a factory. A Tesla factory in Germany will obviously supply at least the whole EU.

No.

There is no convection in the core of the sun. It is plausible that material has mostly stayed there since the formation of the sun.

The only feasible way to have cars and trucks in a zero-net-emission economy is to make them electric. Unless you want to scrap all cars and trucks, the electric versions must eventually be developed and mass-produced.

You weigh one more because you consider the evidence, and not just count the headlines on your feed.

Having seen episode 4-5 now, I think the last episode was pretty good, and the technical breakdown was actually great.

However, episode 4 also wasted an unacceptable amount of time; the intro with the old lady and the pet hunters' parts were heavy-handed fillers, and the time should have been much better spent on expanding more on the different operations (mentioned in a pitiful few sentences in the beginning of ep 4!) and also the biorobots.

One part of my general feelings is summarized well by this article: https://www.newyorker.com/news/our-columnists/what-hbos-cher.... This is basically about grafting a western-style disaster movie narrative onto the story. The other part of my feelings is that they simply did not make good use of the runtime; they wasted most runtime on lackluster invented dialogues.

By "spectacular" I did not primarily mean visual effects, and I think the production value of effects in the series is perfectly okay, I instead meant effective dramatization. I've only seen up to episode 3 now, but I can elaborate a bit on perhaps my biggest specific complaint so far: basically, too much fallback on disaster movie tropes, too much screen time on languid dialogues instead of trying to show much more of the vast amount of documented fascinating stories and details. It should be less about pondering the gravity of the situation with pained expressions, or grave and silent meetings with Gorbachev reminiscent of Hollywood disaster movies; instead the reality of the first few days must have been an absolute frenzy of activity, with massive organizational and logistical challenges, redirecting kilotons of material and equipment and thousands of personnel from all across the USSR. Such challenges are merely mentioned in the episodes, but we get no subjective sense of it, there is no administrative frenzy around Legasov and Scherbina. I am reminded of the Shin Godzilla movie, which is admittedly not realistic overall, but the beginning of it had a spectacular rendition of governmental and military bureaucracy kicked into panicked activity. In comparison, the Chernobyl version is rather dull and stilted. A painful issue with mainstream TV is that there is a core assumption that the audience cares mostly about personal stories but not about technical, procedural and sociological topics, and I get the impression that an HBO show cannot fundamentally break out of this box. Hence, we don't get any information about how radiation actually works and the fundamental mechanisms of its dangers and mitigation, we instead get spooky bullshit about "trillions of bullets".

So, the biggest issue was pacing, script and focus. I could also talk about photography and cinematography, which I think has been fine so far; but I would have been happier with something more creative and adventurous. I've been drawn to the topic of Chernobyl because it evokes a singular feeling of dread and awe. I'm not sure how to best evoke dread and awe; the Chernobyl TV version seemed to have succeeded to some extent, but I think that it only utilized a tiny and conventional sliver of the visual and directorial possibilities.