I read Code of Conduct abbreviated as "see-oh-see." This is also the name of the logic that underpins Coq, the Calculus of Constructions, which I read the same way.
Yes, but I do this so naturally that I often say things like "I'm a Coq expert" when out eating with people I'm close with from my field, and believe me this is not something that works out well for women. People overhear you and at best give you dirty looks, at worst harass you like the driver mentioned in the thread.
I feel you... I'm currently writing my thesis and need to catch myself in time when explaining what I'm doing to people blessed by ignorance. Or alternatively, make the joke right away myself, though that's probably a lot easier to do for me as a guy.
On the other hand, it is kind of hilarious to fall out of your abstraction-tunnel for a moment when citing a source called "A short presentation of Coq".
Anyway, I really feel we need to make at least a few more deliberate puns before they change the name. Maybe just end every sentence referring to Coq in an ambiguous manner with "pardon my French."
There is a free download available for this paper available from the publisher at that link until September 10th. A lot of folks I have spoken to have missed this when looking at the website.
This was a 2+ year collaboration spanning four different universities, with input from experts all over the world. We hope it is useful to others.
All nontrivial programs are riddled with conditional logic. The difference is whether or not this conditional logic is exposed at the type level. Every single time you branch over anything in your code (say, to check if a list is empty before calling a function that will fail on an empty list), you could bubble that branch up to the type level in a full dependently-typed language, and have the compiler do that check for you. (Of course, this doesn't necessarily mean you'd always want to!)
Dependent types can be hard to work with because you have to hold the compiler's hand and tell it that yes, actually, the list you're working with at the point you want to call this function is definitely non-empty, and you can prove it by providing an instance of that type. So if you want to make a function that takes two non-empty lists l1 and l2 and spits back out a non-empty list l3 which is l1 ++ l2, in addition to the standard list append functionality, you need to show that l1 ++ l2 actually is non-empty.
But the fact that you have to do so much of this manually is, in my (professional) opinion, more a limitation of what we can currently automate than an inherent limitation of dependent types.
Sometimes you want the same guarantees, but it's easier to keep this separate from the list type. So you just write plain old vanilla list append, and then later on your inhabit the type that proves that for any two lists l1 and l2, l1 ++ l2 is non-empty. There are tradeoffs here: later on when you need a proof that (l1 ++ l2) is empty, you'll have to explicitly reference the type you found a term for earlier to show it to the compiler. If you put it into the list type itself, then you only need to do that once, when you write the append function. On the other hand, you also have to construct a whole bunch of other functions this way, and you might not actually care about the result being non-empty in those cases.
Also in my professional opinion, switching back and forth between these representations will be easier very soon. There are probably dozens of fantastic researchers all over the world working on making this easier, and we've made a lot of progress these past few years!
Regardless, deciding what you actually want to expose at the type level and how you want to expose it is an important design problem, and it depends a lot on what you want to be able to prove about your system without ever running your code.
