perthmad

5 ms·

1.
by perthmad 1y ago
This integer only exists if you assume classical logic. Otherwise, there is no such integer a priori, and actually there is none in general.
2.
by perthmad 1y ago
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 c
3.
by perthmad 2y ago
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 u
4.
by perthmad 3y ago
Any algorithm you do not understand.
5.
by perthmad 3y ago
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-negatio
6.
by perthmad 6y ago
> 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
7.
by perthmad 6y ago
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.
8.
by perthmad 6y ago
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
9.
by perthmad 6y ago
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 notab
10.
by perthmad 7y ago
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".
11.
by perthmad 7y ago
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
12.
by perthmad 7y ago
"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", r
13.
by perthmad 7y ago
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.
14.
by perthmad 7y ago
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,
15.
by perthmad 7y ago
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 En
16.
by perthmad 7y ago
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 tha