the_benno

If you're interested in this kind of thing, definitely also check out the upcoming HOPL conference -- co-located (whatever that means for a virtual conference) with PLDI this June. Matthias was on the program committee, along with a bunch of other PL OGs.

Website: https://hopl4.sigplan.org Papers: https://dl.acm.org/toc/pacmpl/2020/4/HOPL

In PL academia (including in the US) many people prefer dot paper for physical research notebooks. When you're mixing together diagrams, prose, inference rules, semantics, code, etc. it's a quite nice and flexible medium.

Thanks, I'll dig in some more. Perhaps I'm unfairly projecting onto Mounk and conflating his work with that of other "intellectual dark web" types and their fakakta cancel-culture takes. I haven't followed him closely since the flurry of discussion/debate when the project launched last summer.

Personally, I'm a little less convinced of the 1st bullet point.

In particular, I see many obstacles to a "free society in which everyone gets to pursue a dignified life": healthcare costs, ongoing climate disaster, erosion of labor rights, rising nativism and authoritarianism on the far-right, etc. chief among them. To be as monomaniacally focused on "cancel culture" as Mounk (and many others on the center/right of the American political spectrum) strikes me as misguided at best and disingenuously self-serving at worst.

Persuasion seems to me a massive over-reaction to the minor injustice that is "cancel culture" wrapped in some self-important and grandiose rhetoric.

Many SE research papers include a "threats to validity" section which is more or less what you're describing

Cops aren't allowed to murder people on sight -- "junkie" or otherwise. Never understood why people seem to think this is a compelling argument.

A very cool and surprising result that I always thought should've received more fanfare in non-PL circles.

Just as a little extra context on what "unsound" means here since the term is often misused or used in different contexts: this program violates "type soundness", which is informally stated as "well-typed programs don't go wrong".

Generally you'll see this shown via a "progress" lemma (~ "all non-value expressions can take a step in the operational semantics") and a "preservation" lemma (~ "expressions' types are unchanged by the operational semantics") which, by induction, yield a theorem like "all expressions of type T can be evaluated to a value of type T" (for all T).

This paper, since it deals with actual programming languages and not minimal calculi, may feel a little bit removed from the theoretical stuff, but under the hood it's the same idea: preservation doesn't hold when applying `coerce`, so well-typed programs _can_ go wrong.

There's some great discussion in Section 6.3 about the (abundant!) literature on Java subsets/core calculi, and both the benefits and limitations of using such languages to reason formally about actual PLs.

I can confirm that the second edition gives a quite-good treatment of data flow analysis. Not as thorough as you'd find in a proper program analysis book (where Nielson is the usual choice, though the recent Rival/Yi book on abstract interpretation is fantastic IMO) but it's well-written and at around the right level of detail for a compilers course.

Source: PL PhD candidate, used (parts of) it to teach a graduate compilers course.

Yes, what you call minced beef is called ground beef in America. Not to be confused with mincemeat, though, fellow Americans! I was very confused the first time I had that in the UK.

We built an effect system to enforce thread safety in Rx-based android apps a few years ago and published a paper on it at ASE, if you're interested: plv.colorado.edu/benno/ase18.pdf

the idea should generalize to whatever thread-pool/effect constraints you want to express, but the paper and implementation are focused on keeping UI effects on the android main thread.

As a 27-year-old CU PhD student and staff member, I just want to say that this is a welcome development. The university recklessly opened this fall without adequate security measures in place over the loud protests of faculty and staff, and (surprised_pikachu.jpg) now Boulder is facing a massive outbreak clearly attributable to campus' opening [1].

My friends, colleagues, and community are being directly endangered by CU's obfuscation of case data, refusal to provide comprehensive testing, and foot-dragging on promised safety measures. It's ridiculous that the city/county are being forced to mitigate the downstream effects of this doomed-from-the-beginning plan, but the "run it like a business" university administration is a lost cause.

[1] https://www.bouldercounty.org/families/disease/covid-19/covi...

This seems like a kneejerk response to a strawman version of Zinn. He's a pretty middle-of-the-road academic politically speaking and doesn't get anywhere near what I would call far-left.

As for "pessimistic", well, I'd just say that the facts don't care about your feelings. Powerful institutions are (generally speaking) violent and uncaring towards those without power; ignoring that fact does us all a disservice.

Yes, this is an extremely active area of research with lots of connections in the broader programming languages and formal methods communities. For the last decade or so, POPL has had a co-located workshop on proof, the programs of which would be a great place to see the current state of the art. Here's last year's: https://popl20.sigplan.org/home/CPP-2020#event-overview

Wind Waker on the gamecube is a perfect example of what you're describing. Almost 20 years old and I still think the cel-shaded graphics look great, especially when compared to its more "realistic" contemporaries.

This is a beautiful paper that anyone interested in abstract interpretation and sound static analysis probably already knows, but the core idea is quite accessible.

An abstract machine is a formalization of the concrete semantics of a programming language, and we'd like to be able to "lift" that concrete semantics to an abstract semantics: a finite (and therefore computable) over-approximation of program semantics.

However, the concrete structures of an abstract machine (most notably continuations) are themselves potentially infinite, so you can't just build a "structural abstraction" by applying the abstraction function pointwise over concrete structures -- the resulting abstraction is infinite and thus static analysis may diverge.

That's where this paper comes in: its key insight is that, by store-allocating continuations and bounding the number of store addresses, you can finitize an abstract machine such that structural abstraction works out nicely while preserving the underlying semantics.

This is an awfully confident statement that is unsupported by available evidence on covid transmission and health risks. On what basis do you say that in person classes are completely safe when reopening of indoor spaces has led to massive upticks in infections across much of the US?