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....
My understanding is that this shows how vanilla Coq still can’t encode quotients well. This project relies on a PR [0] that breaks term normalization, which makes it highly unlikely it will be merged. My understanding is that Lean’s implementation of quotients also breaks normalization, but they don’t care as much about that as Coq devs do.
The normalization issue is not about quotients at all. It's https://arxiv.org/abs/1911.08174 "Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality"
Why isn't good stuff like this not more upvoted, but Ross Ulbricht post are simply deleted while I can't delete my comments from 2012 (accname: mkorfmann).
Cheerio and you're fun at parties Paul, enjoy that Gin Fizz
Very nice work. This kind of embedding (a direct equivalent to "transpiling" for code) is quite common in the formal methods community; for example, Freek Wiedijk has shown a similar embedding of HOL Light https://www.cs.ru.nl/~freek/notes/index.html into Coq.
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).
I don't think this is correct - coq does not have a /u/ sound in /cok/ but coke is pronounced /couk/ (sorry for the completely unortodox phonetic language).
Well, it entirely depends where you live. The GP's comment make perfect sense where I am, and seem a good explanation, but sure, depends on how you pronounce 'coke'!
Not trying to be childish, but let's be honest, this is a horrible name if you are not a native english speaker. I just hear giggles every time somebody mentions this name...
This is a horrible name even for native english speakers. I still have to coach people not to giggle whenever I bring up LaTeX - unless it's exclusively vocally in which case the "lah-TECH" puts their mind elsewhere.
... in some (BDSM fahig?) circles? I know it's used there, but there are quite a lot of other things I think of before that. And some colleagues I just asked as well.
I kinda miss those times where you could talk about those Thinkpad clits at work and no one would bat an eye. The degree of puritanism of the new generation is a bit terrifying.
I don't think it's puritanism, it's just keeping things separate. In an office we're all there to work and not get embroiled in relationship drama - so calling that nub a clit is just unnecessarily bringing sex into things.
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.
Coq means a rooster in French that is not a usual name for theorem prover by itself. Therefore Coq developers should have thought that it is at least an interesting (and more likely, funny) idea to name it after an animal, much like CHICKEN Scheme.
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.
I'm not sure. I don't really know these people or the project history. I balked last time and was emailed by somebody who told me they were familiar with the project/team, and they said it was well know about the double meaning.
I think it is incredibly inappropriate in a field that already has sexist anti-female issues.
While they talk about "prudish" Americans, they can be sexist assholes; they can go fuck off.
These guys shouldn't be supported. Tech already has enough issues with sexism and female participation. This doesn't help the situation at all. I expressed the same opinion last time, and will flag this all day long.
The more powerful our languages get and more robust our programs written in them get (those go hand in hand), the easier it will be to compile languages from one language to another without compromising code quality or legibility.
I hope this will lead to a new golden age of programming and PL research where more software is not "trapped" in the language and era it is first developed, and we aren't constantly bouncing between the extremes of endlessly accumulating tech debt or naively rewriting.
> The more powerful our languages get[...], the easier it will be to compile languages from one language to another
I'm not sure about this. Don't languages get their power from restrictions and opinionatedness, that create a fundamental impedance mismatch between any languages that aren't redundant? You can do anything the processor can do in assembly, and the unstructured mass is about as powerful as muscle with no bone.
But maybe I'm reading "powerful" too positively. As languages get kitchen-sinky, as JavaScript/C++/Java are with reckless abandon, it will be easier to use them as translation targets (and harder to reason about the results). But won't kitchen-sinky languages eventually give way to languages that haven't yet had time to tie themselves in knots, as C++ (which finished the kitchen and is now putting a second sink in the bathroom) is losing ground to Rust (which only just bolted on async), in an endless cycle of collapse and renewal?
36 comments
[ 6.1 ms ] story [ 89.8 ms ] thread[0]: https://github.com/coq/coq/pull/10390#issuecomment-554316311
My understanding was that these features are how quotients are managed to be implemented. But perhaps that is wrong.
Cheerio and you're fun at parties Paul, enjoy that Gin Fizz
[1] https://deducteam.github.io/
[2] https://github.com/Deducteam/
[3] https://github.com/Deducteam/CoqInE
[1] https://hal.inria.fr/hal-01840643/document
Well, it entirely depends where you live. The GP's comment make perfect sense where I am, and seem a good explanation, but sure, depends on how you pronounce 'coke'!
We had plenty of women in the lab, btw.
Usually and fortunately though, the average person simply grows up and stops giggling at the word quite quickly. And so do Coq users.
[1] https://www.call-cc.org/
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.
I think it is incredibly inappropriate in a field that already has sexist anti-female issues.
While they talk about "prudish" Americans, they can be sexist assholes; they can go fuck off.
I hope this will lead to a new golden age of programming and PL research where more software is not "trapped" in the language and era it is first developed, and we aren't constantly bouncing between the extremes of endlessly accumulating tech debt or naively rewriting.
I'm not sure about this. Don't languages get their power from restrictions and opinionatedness, that create a fundamental impedance mismatch between any languages that aren't redundant? You can do anything the processor can do in assembly, and the unstructured mass is about as powerful as muscle with no bone.
But maybe I'm reading "powerful" too positively. As languages get kitchen-sinky, as JavaScript/C++/Java are with reckless abandon, it will be easier to use them as translation targets (and harder to reason about the results). But won't kitchen-sinky languages eventually give way to languages that haven't yet had time to tie themselves in knots, as C++ (which finished the kitchen and is now putting a second sink in the bathroom) is losing ground to Rust (which only just bolted on async), in an endless cycle of collapse and renewal?