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