perthmad

This integer only exists if you assume classical logic. Otherwise, there is no such integer a priori, and actually there is none in general.

Any algorithm you do not understand.

> 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".

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.