nmrm2

> There's a stark difference between a free and voluntary association of like-minded people and a so-called "safe space"

No, there defintionally is not... perhaps there seems to be a confusion over definitions.

The fact that people want to expand the rules governing a particular safe space into a large sphere doesn't change the definition of a safe space.

You can take offense with someone wanting to make a classroom into a safe space, but I really don't get why any non-authoritarian person would insist on not allowing safe spaces at all.

Also, I'd be surprised if OKWU faculty/students/alumni don't try doing the exact same thing (expanding the boundaries of their safe space) by voting for fundamentalist christian politicians who enforce christian morality on women who use birth control, homosexuals, people who consume alcohol, etc.

> ...which uses a pretext of "victimization" to capriciously thought control others who simply committed the offense of disagreeing or criticizing.

What, like kicking someone out of a university when they realize half way through a difficult-to-transfer course of study that they're gay? Or that they enjoy square dancing?

The harm that fundie universities like OKWU have done to students who disagree ever so slightly with their idiotic version of religion is demonstrable and significant. Your argument that students somehow "should have known better" is, IMO, fundamentally misinformed.

> And this is evidence of what, exactly?

That OKWU is a safe space and that safe spaces have always existed, but they usually function to shelter people who are aligned with popular opinion / cultural norms. You know, like social norms (e.g., not employing publicly out gay people, looking the other way when transvestites are assaulted, etc.) protecting homophobes from having to knowingly interact with the icky gay people.

OKWU is a safe space for people who don't want to have to interact with anyone who does not subscribe to their particular brand of nutty American puritan christianity. It's a place where people can be openly homophobic and openly judge other people's sexual morality without being socially ostracized like they would be in the real world.

Just in case my opinion isn't clear by now: Everett Piper is a massive hypocrite who runs a religious commune with strict codes of conduct while also appealing to liberal values. He doesn't actually give a shit about free speech or dissenting opinions. It's impossible to take someone seriously when they claim universities aren't safe spaces while also expelling people for disagreeing with a very particular and very whacky form of christianity.

For the third (!) time, modus operandi matters.

Coq's huge library of tactics and proofs of facts that TLA+ might just throw at a model checker are, in my experience, very useful starting points for things that can't be model checked.

Ostentibly TLA+ could build up an equivalent library of tactics and proofs.

> Why low opinion?

Even supposing type theory is "more obscure", it's pretty hard to believe that someone could study it for 30 years and not understand it better (in some sense) than ZF. That's a pretty extraordinary claim.

> basic set theory -- the one that barely scrapes the definition -- is all that's required to specify real-world programs.

Not really -- you often need non-trivial constructions when proving properties about rewrite systems within set theory. Those constructions are much harder to understand than induction on algebraic datatypes, which is why type theoretic approaches have dominated in formalization of programming languages.

>Unless I'm missing something...

I'm disinclined the dismiss separation logic just because you can code up some of its ideas in another logic (in a way that counts as a novel contribution worthy of publication, no less).

The clarity with which separation logic presents the idea and use of the separating conjunction has obviously influenced the paper you cited. I would think this is reason enough to summarily dismiss these "everything's a TM"-style arguments you're making here. The authors of the paper you cited are only not using separation logic in a kind of meaningless sense IMO.

> So far, I don't see why I should.

This sentiment kind of reminds me of people who have never typeset mathematics complaining that LaTeX is useless... which is to say, perhaps you simply aren't interested in and so don't care about the use cases where Coq shines? Lots of people -- including me -- have already pointed out a lot of these use-cases in this comment section.

But really, based on the arc of this conversation, I would be enormously surprised if you chose to use Coq to prove X, even if there were a proveX tactic already written in Coq and the TLA+ implementation would take all day ;-)

You act as if "conscience" is an objecively good thing, and not just the result of a bunch of totally arbitrary social expectations.

Gay people who grew up in conservative families often have a conscience that makes them feel bad about being gay. Gay people looking for safe spaces where they aren't reminded that they spent 18 years being told they are bad people is imminently reasonable.

Abused wives often feel guilty about leaving their husbands. Finding safe spaces where they don't have to feel guilty about doing the right thing is imminently reasonable.

So, no, it's not unreasonable to find places where you don't have to "deal with your conscience"

Like I said, modus operandi matters. If I have to perform another model checking routine (possibly on an infinite state space) to slightly generalize a theorem, then in many cases that means I never really had a useful proof of it in the first place.

Also, Coq's mathematics library is extensive and often closely follows the proofs found in graduate mathematics text books. Last I looked into TLA+, it was squarely focused on algorithms and hardware (not even CS-related mathematics more generally -- specifically algorithms and hardware).

> So you think some people are more familiar with type theory than with undergrad-level set theory (ZF)?

Do I think there exists some population of people who are "more familiar" with type theory than with ZF? Yes, starting, for example, with every researcher whose primary area of study is type theory. In fact, I think that anyone who doesn't honestly believe there are such people must have an extremely low opinion of quite a number of very smart people.

(Also, set theory qua set theory gets really disgusting and kludgey really quickly, and is something that almost no undergraduate (or even phd student) is exposed to these days. The "set theory" you see in a discrete math course kind of barely scrapes definitions. I think most people who posit that "set theory" is nice and simple must've never really dove deem into the actual theory of set theory...)

(Also, most real math these days quickly abstracts away from germanely set theoretic constructions. Mathematicians don't work in ZF. They do not. Most will tell you they do not, if they even know what ZF is. Which a lot won't, because their undergrad discrete math course is probably the last time they saw a truly formal derivation. And the mathematicians who do know what ZF is often can't regurgitate an axiomatization of ZF. If you tell a mathematician that all of math is just set theory, most will chuckle and wink and say "why, yes, yes it is", and hopefully you're in on the joke...)

> I don't see it... I fail to see anything that isn't readily expressible in simple classical logic + temporal logic. Could you explain?

Did you read this dissertation's explanation of why separation logic is important?

To the extent that this observation is remotely reasonable, it's only in the sense that you can code up one logic in another. Which, well, all the world's a TM, as they say...

Anyways, I think the argument over whether type theory is a successful foundations for CS research and practice is already a closed issue. It demonstrably is. So is set theory.

It's one major advantage, yes. And not just for the sake of software verification. Sometimes when proving a non-CS-type-math theorem you still want an efficient implementation of an existence proof.

But code synthesis is a lot harder than merely being constructive, and efficient code synthesis even more so. Use cases for Coq that depend upon code synthesis don't come for free just by avoiding LEM. So although it's fair to say that you can do classical reasoning in Coq, I'm not sure saying you can do synthesis from TLA+ if only you avoid LEM is fair at the moment (I might be wrong).

> Are there any advantages to using dependent types?

Here are a few other reasons for using Coq:

* Proof terms. There are two major disagreements here. The first grounds out in philosophy and the second basically amounts to "you really want to compose the proofs and make sure they are still a proof instead of just throwing away the proof and using the theorem" which has lots of good systems-y justifications

* Specifically wrt TLA+, Modus Operandi matters. If you want a formal proof in the typical sense of the word (rather than a verification of fact based upon model checker output), then Coq userlands's tactics and theorems are useful.

* Lots of people like to disparage the amount of algebra that FPers talk about. But it turns out that if studying those algebraic structures is your day job, the relationships between types and algebraic structures makes type theory convienant.

>simpler, more familiar

This is almost definitionally subjective. Which isn't meant as a criticism, in-so-far as one realizes that other people might have different experiences and so might (just as validly) consider other formalisms more familiar.

> and more flexible

There are (obviously) a lot of people who fundamentally disagree with the concrete arguments Lamport makes in this paper. I wish someone would annotate the paper with references to literature from the type theory community that address some of his concerns.

For the record, I don't disagree with Lamport. I think Lamport is right -- for some use cases, it certainly makes sense to stick with ZF. But he's also wrong -- sometimes, the type theoretic approach really is simpler, more familiar, and more flexible. E.g., in the case of this dissertation.

There is a self-contained book; IMO chapter 1 gives a good overview of what you should be comfortable with:

http://research.microsoft.com/en-us/um/people/lamport/tla/bo...

Also, formalizing architectural properties for the world's most popular cloud service is probably even rarer a task than formalizing language specifications.

The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications.

What matters is that important libraries and frameworks can be verified, not that everyone and his brother can use formal methods for every WordPress website they churn out.

The characterization in pron's post is decidedly biased toward TLA+ in a way that I think is unnecessary. A few correctives:

* Coq has seen plenty of industry adoption. To say that type-theoretic theorem provers (or the Coq system specifically) are merely academic toys compared to TLA+ is wrong.

* "Normal" mathematicians (not just "weird Computer Science-type" mathematicians, whatever that means...) have used and extolled the virtues of Coq as a tool as well as its theoretical foundations. See e.g., the univalent foundations project. Regardless, I'm not sure I understand why "Computer Science-type math" is an unreasonable foundations for a program specification tool, which is what TLA+ is. And if the goal is formalized mathematics, you're probably better off with Coq (and it's not even clear that the TLA+ community is interested in that sort of thing, independnet of results useful in the course of a program specification/verification task.)

* If you're familiar with (esp. typed) functional programming, you might find Coq even easier to get into than TLA+. On both sides of the type theory vs sets/axioms divide, people should be careful not to confuse one's predispositions based upon educational background with the actual mental load of learning to use a tool.

There is room for both of these tools (and more!) in the world. I don't understand why they have to be in competition. A formalization of the C standard is a HUGE undertaking, independent of what tool was used. Let's celebrate that achievement!

It's not that there's anything wrong with using a high-level language for safety-critical systems with real-time requirements and limited hardware. It's just that every high-level language that's remotely appropriate for this set of requirements wasn't production ready (or even conceived of) 10-20 years ago.

Hopefully the next generation (or the one after that) of control software for aircraft will be written in beautiful code :-)

Says killface?

Also, absolute limitations on page count is really common in CS, and the page counts tend to be pretty low. In other areas, journals might allow for more citations or citations might not count toward page count.

Also, arxiv is physics-biased.

In general, there's a cogent argument to be made that some of the more extreme predictions people have made about the ultimate impact of global warming are maybe a little bit over-dramatic (and in fact, some prominant climate scientists called out Sanders for this). But this guy? Nutjob.

In technical fields (which is what this article is about)?

The ones who choose to stay in academia and are lucky enought to find a position are called "Professor".

The unlucky or disillusioned ones -- as well as the (majority) of PhDs who never even intended to go into academia at any point during thier studies -- are called, variously, "Engineer", "Analyst", "Consultant", etc. and typically start in the low six figures (and not even in the bay area / NYC). They take a marginal hit to their lifetime earnings, but in most cases make decent salaries and get to work on more interesting problems (obv. interesting is subjective).

> Unemployed.

The unemployment rate for STEM PhDs is ludicrously low (FYI: if you google this, be aware that the Slate article by Jordan Weissmann is IMO purposefully misleading. See Table 1 of http://www.nsf.gov/statistics/infbrief/nsf14310/ and compare to his graphs. E.g., his graph seems to indicate that the unemployment rate for CS PhDs was over around 15% in 2001, but the NSF tables makes it clear that the rate was 0.9%, which is even more than what most economists refer to as full employment. In fact, in CS, the increase for 0.9% to 2% is almost entirely attributable to there being a lot more retired CS phds now than 10 years ago (for rather obvious reasons). So the stats he's using to tell his story are, at very best, unintentionally but absurdly non-representative of the actual state of affairs. It's like asking someone the day after they quit their job if they've started their new job yet and, when they say "hell no, taking some time off to recharge", assuming they're unemployable and/or don't have something lined up.)

Of course. You can most anything without a degree, with very few exceptions (see: the article).

But the degreed : undegreed and phd : nonphd ratios in language design/compiler implementation are much higher than in software development more generally. The same is true of other technically challenging things. If you agree with that observation, then I think we're violently agreeing or you're reacting to the tone rather than the substance of my post.

> Would you care to provide them?

Anecdata, and bearing in mind that "originator of a language" is a very, very small subset of all people working on compilers / language design (and that even there, I think my observation holds -- especially for degreed : undegreed, and probably even for phd : nonphd). And that compiler/language design is only one very small segment of what a reasonable person would consider to be core infrastructure.

I don't have the time or the interest to run this study. Feel free to do so.

For instance, the sentence right after the one you quote ends with: "...or really extraordinary dedication". The handful of people you mention in your post, I think, count as extraordinary.

To reiterate my point:

The IT guy who helps hack out some spreadsheets isn't an actuary. The nurse who changes sheets isn't a doctor. But in software, there's no distinction -- in terms of externally recognized job titles -- between the guy hacking on wordpress templates or apps that burn my phone's battery and steal my data for no reason, and someone working on a piece of critical infrastructure.

I can't really respond to your anecdata without starting a flame war, but suffice it to say that perhaps some people would consider PHP or Perl or JavaScript cogent counter-examples to the point you're trying to make.

Finally, lots of actuaries without degrees rise to the top of their organizations and get to work on really cutting-edge stuff. Those people are extreme outliers. The same exact thing is true in software. Literally the only difference is that actuaries don't have the same sort of blindness to statistics that software people do, and I think the reason is that there's a clearer distinction between "grunt work related to actuarial work" and "professional-grade actuarial work".

If we made that distinction in software, then I think the perception that you can do real software engineering without a degree would shift far closer to "Exceptional" than it is now.

Yes (edit: accidentally said the opposite of what I meant!). What you need to be able to do is pass the exams. BUT -- plenty of people with math degrees fail these exams. It's a hell of a lot harder than learning how to hack together a RoR site.

See e.g., various discussions on http://www.actuarialoutpost.com

You can also e.g., fill a number of supporting roles around actuaries without a college degree and then demonstrate competence by taking exams.

> I wonder if maybe software developers are a little more inclined, as a "profession", toward paths that are less formalized.

I think the fact that everyone in software has the same job title makes a huge difference wrt medicine and engineering.

The guy hacking together cookie-cutter single server websites calls himself a software developer/engineer just the same as the Ph.D. hacking on compilers or ML algorithms. Everyone inside the field knows there's a huge difference between these two jobs, and that becoming the latter is basically requires a degree (perhaps even an advanced one) or really extraordinary dedication while the former probably doesn't even need a degree at all.

So when someone says "do I need a degree to become a software developer? / Is a degree the fastest path to becoming a software developer?", it's an ill-defined question. What do you mean by software developer? Do you want a good salary doing whatever in boom times or do you want to do really technically interesting work with job security even in bust times?

Conversely, most other fields tend to differentiate between job titles that require lots of skill and jobs that don't.

For example, the difference between various levels of non-doctor healthcare workers (the whole range of nurses, and then everything up/down from there) is very institutionalized. Something similar happens in engineering -- plenty of non-engineers do engineer-y things in engineering firms, but some things you'd be insane to delegate to someone who doesn't have formal engineering education.

So do most practitioners in careers that are typically associated with or require a university degree: actuaries, accountants, engineers, lawyers, doctors, teachers, etc. all have to stay current with their respective fields and do so primarily through self-study.

Of course there exist people in all of those careers who don't. But the same is true in software.

If you're building a company, odds are you aren't doing fundamental research (and you might not even be doing translational research).

Even by the second page of the paper it's very clear the study is designed to read off intrinsic motivations, both value-laden and pure enjoyment:

This framework also accounts for potential interaction effects between intrinsic and extrinsic types of motivation. For the intrinsic and extrinsic motivation subscales, 36 items are included in our questionnaire. Each subscale (i.e., enjoyment based intrinsic motivation, self-reinforcement, obligation-based motivation, integrated regulation, identification, introjection-based regulation, external regulation) consists of four to eight items...

The real question (which the authors are silent on and the journalist helpfully mischaracterizes) is whether these researchers' results generalize to non-R-ecosystem OSS development.

Here's why I think this work doesn't generalize: Academics and people who don't primarily identify as software engineers are over-represented in the R community, when compared against other open source projects. I think the set of answers you'd get from e.g., the developers of more traditional types of open source projects (editors, compilers, databases, games, OSes, frameworks/libraries, etc.) are fundamentally different.

While I'm on my soap box, the other mistake that researchers who study open source developers often make is focusing on very successful open source projects, and then implicitly or explicitly generalizing those results to the huge hoard of open source developers. (Implicit generalization goes something like this: Intro: there are so many open source developers -- understanding their motivation is important! -- Actual study: let's look at the motivation of contributors to the top 1% of projects -- Conclusion: we think these results generalize to other projects. Note that the authors of this study avoid this pattern, but the journalist doesn't.) But of course, the motivations of the vast majority of OSS developers are going to be fundamentally different from those developers who have built extremely successful and high-profile systems.

Overall, I think this is a really nice and interesting paper about the R ecosystem. I just wish the journalist had chosen a different headline and lede.

We all know that different ecosystems typically have different values.

But more importantly, R developers are particularly non-representative of the more general open-source ecosystem. Based on anecdotal evidence, I believe it's highly likely that academics and people who primarily identify with non-CS fields/disciplines are over-represented in the R community when compared to other communities.

(Note: At least within the text of the paper, the researchers DON'T claim that their results generalize to all OSS developers, and don't even claim their results generalize to all R developers!)