This integer only exists if you assume classical logic. Otherwise, there is no such integer a priori, and actually there is none in general.
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…
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…
Any algorithm you do not understand.
Proving a negation is not a proof by contradiction, that's just the proof of an (absurd) implication. Logic people actually write blog posts about this: https://math.andrej.com/2010/03/29/proof-of-negation-and-pro...
> 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…
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…
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.…
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".
On that particular topic, I definitely recommend reading François Héran's 1991 article "Pour en finir avec « sociétal »" [1]. [1] https://www.persee.fr/doc/rfsoc_0035-2969_1991_num_32_4_4079
"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…
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…
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…
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…
This integer only exists if you assume classical logic. Otherwise, there is no such integer a priori, and actually there is none in general.
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…
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…
Any algorithm you do not understand.
Proving a negation is not a proof by contradiction, that's just the proof of an (absurd) implication. Logic people actually write blog posts about this: https://math.andrej.com/2010/03/29/proof-of-negation-and-pro...
> 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…
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…
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.…
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".
On that particular topic, I definitely recommend reading François Héran's 1991 article "Pour en finir avec « sociétal »" [1]. [1] https://www.persee.fr/doc/rfsoc_0035-2969_1991_num_32_4_4079
"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…
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…
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…
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…