It's a satire of a typical kind of paper from logic, in particular modal logic. Jean-Yves Girard has been very vocal against these academic papermills where the authors consider ad-hoc meaningless logical systems. For a more in-depth critique of semantics, you can also read the broccoli logic paper: https://girard.perso.math.cnrs.fr/meaning1.pdf
It reminds me of this weird theory about proto-Castillan. According to some scholars, the change from initial /f/ in Latin to /h/ in Spanish could have been caused by the bad teeth of the speakers of lore, a phenomenon ultimately due to the water quality in some areas.
> Typescript actually has an insanely powerful type system
I think you are conflating expressivity with complexity here. You do not need a complex type system to get a very expressive language. For instance, the typing rules of dependent type theory are fairly simple compared to the amount of trickery needed to make TypeScript work.
At constant expressivity, a simple type system is always preferable to a complex one. So I am not amazed by the fact that TS needs advanced PLT debauchery to kind of work. It doesn't even give you strong guarantees. There is a reason why Hindley-Milner type systems are called the sweet spot of static typing.
The phenomenon described in this article is actually an instance of Reynold's parametricity. This one of the free stuff you get for using a (reasonable version of) static typing.
Nah, I agree with Hobsbawm in "The Short Twentieth Century" that the previous century ended in 1989, with the fall of the Berlin wall. Since then we've been observing the heyday of neoliberalism, fueled by a lack of a serious contender.
What do you mean? CoC definitely supports impredicative encodings, and as far as expressivity goes, this allows to implement a lot of programs. Proving them correct is another matter, but that's not what you implied. Also, CIC is notably not Turing-complete.
It's even clearer when you consider higher-order functions. These diagrams are only able to represent functions of order at most 2, i.e. what is called "dependency injection".
"Jour" is polysemic, it literally means "day", but metaphorically it also means "light". For instance, "voir quelque chose sous un nouveau jour" means "to see something under a new light", rather than "a new day".
You can actually do much better than mere embeddings. Using program translations similar to what Haskell users routinely perform when using the do-notation for monads, you can actually extend your type theory with new reasoning principles. See for instance the parametric exceptional theory [1], which adds well-behaved exceptions and allows to extend Coq with the independence of premises, i.e. (¬A → ∃n:ℕ. P n) → ∃n:ℕ. (¬A → P n).
Define "the authors". Gérard Huet, who wrote the software almost 35 years ago was definitely aware of the meaning, and indeed this was done in order to overtly piss off the prudish Amercians.
In the current core development team, I think it is reasonable to say that most people range somewhere on a scale from "don't care" to "mildly annoyed". Amongst the annoyed group, some actually advocate for a change of name.
For the record, French speakers also have at first a hard time with the "bit" word that is usually pronounced at the very beginning of any introductory CS class. Indeed, it has the same figurative meaning as "cock" in English. Worse, you can find it in compounds such as "32-bit" or "bitfield", so try figure out the evocative power of those expressions.
Usually and fortunately though, the average person simply grows up and stops giggling at the word quite quickly. And so do Coq users.
This particular feat was triggered by Kevin Buzzard's unsubstantiated claim that "Lean was better than Coq" as a foundation for mathematics, because it had built-in quotient types. The work described above precisely shows that such types can be encoded as well using features shipped with the vanilla Coq distro. See https://sympa.inria.fr/sympa/arc/coq-club/2020-01/msg00006.h....