jonsterling

Does anyone know what that borderless terminal is?

I do pure type theory, semantics, proof theory & intuitionistic mathematics. Very little of this will find a home in industry (at least, not for several decades). Industry has historically been incredibly resistant to 100% of the things I'm interested in, and I don't blame them!

But it's not just the hard & expensive stuff that they are resistant to. Even the "easy" stuff (like adopting a programming language designed by the professionals instead of the amateurs) they won't do.

I build interactive proof assistants. But I'm not pushing their applicability to industry, and I don't expect them to be relevant to industry (for a long time at least). Why? Because it's too expensive. Formal verification in type theory MAKES NO ECONOMIC SENSE; ask anyone who's actually ever done any industrial verification, and you will find out what tools they are using, and it has nothing at all to do with the area of research I'm involved in. This is because there are inherent trade-offs in every technique, and industrial use-cases tend to prefer a certain set of trade-offs, and I prefer a different one.

But it's a fascinating topic, and something that I'm preparing to devote the next several years of my life to. And I can safely say that a meteorite will more likely destroy Manhattan than will any of my computer science research be of widespread relevance to industry.

So, no, I totally disagree with everything you have said.

Who gives a damn if academic research is relevant to industry? Almost anything that could possibly be relevant to industry is highly uninteresting.

Imagine being someone who thinks that Capital could decide what is a good problem to work on...

Having enough money that you can value time over it is associated with greater happiness.

it's nice for the haskell folks that they'll be getting some sort of dependent types, but suffice it to say that they will be of a very different sort than the Idris ones.

Not to mention, there is hope of giving a semantics to Idris since it is based on a fairly routine variant of type theory, whereas I don't think there is any hope at all of understanding "which" type theory the Haskell folks shall have implemented.

It's a matter of behavioral type theory vs structural type theory; each can benefit from "slapping a solver on", but behavioral type theory allows you to reason directly about the code from a partial and effectful language, whereas structural type theory does not (in a direct way, at least).

Lean, Coq and Agda all implement structural type theory.

One option is to treat the solver as a trusted "black box" rule if the user wants to—so theoretically, you could get all the benefits of something like Liquid Haskell simultaneously with the unbounded expressivity of full Nuprl.

Nuprl is absolutely still actively developed, in fact; I am constantly in touch with the PRL group. But the code-base is very crufty. In the past two years, though, numerous features have been added (including nominal abstraction, exceptions, bar induction, and a number of other interesting things), which you'd be aware of if you spent more time paying attention and less time snarking.

I am not at all telling people, "Switch from Liquid Haskell to Nuprl!". I'm providing perspective on the design space.

There's a perspective that unifies both the Liquid Haskell-style approach and dependent types, which is "behavioral type theory". Nuprl (the longest-lived implementation of dependent type theory, starting in the early 80s and still going strong today) is an example of a behavioral type theory, for instance; it's a trivial example, though, since the behavioral types refine a unityped structural framework, but you can generalize it to get something along the lines of Liquid Haskell, but without being tied to a solver. This is what we are currently working on with the JonPRL project; we have so far implemented a Nuprl-style type theory, and the next version of JonPRL will have a structural type theory underneath it.

Springer books are great—but academic publishers are widely reviled.

It is no wonder that Chomsky didn't treat him as an equal, given that Sam Harris is really in no position to discuss anything with him...

Well put.

Presumably working on their syntax and semantics. PL is a pretty broad field that encompasses proof theory, formal logic, language design, compiler design, etc.

Just make sure your phone is charged, since you'll look like a real douche if there's an emergency and you need to call police/ambulance with your dead phone that you've just been talking on...

Ugh, Old Persian? Lame

They should pay me the big bucks to translate tweets into Akkadian or Sumerian.

Screw that guy; love that the "disgruntled" workers took action.

I don't know, that sounds pretty out of touch. Pretty much no spam ever is something someone's going to be tempted by. People can get fooled by spam, but if they know enough about how to eliminate all sources of advertising from their life, they're not likely to accidentally sign up for a penis enlargement pill program.

What does advertising and phone spam have to do with anything?

Yes, I know it! This is beside my point, but it is of course definitely true.

Every implementation in Okasaki is easier than an analogous imperative/ephemeral one. Every single one.

somebody had to say it

type theory has broad applicability, since it serves as the basis for all modern programming languages design and research. another nice example is kripke logical relations, which can be used to give a model for a programming language in which you can prove certain safety lemmas for critical code.

What a lovely post! Still true.

Another great post that he links to is Persistence of Memory (https://existentialtype.wordpress.com/2011/04/09/persistence...) where he talks about persistent and ephemeral data structures, and gives a convincing argument for the former.

There are a number of good points here, but I am surprised by the fact that John wants a global coherence check, since in our conversations he has always insisted on the primacy of local reasoning.

Just FYI, "Beluga" also refers to a proof assistant based on the logical framework with contextual modal type theory: http://complogic.cs.mcgill.ca/beluga/

Yeah! We did really well; your mileage may vary, but at the time I was there, you could definitely get a 2-3 bedroom apartment within 1.5mi of campus for less than 2000. I was in Elmwood (a nice little area right on the border of Oakland). Not sure how it is now (but it has only been a few years).

Verificationism is still alive and well, but perhaps not as a basis for empirical science...

Following Gentzen, Dummett, Prawitz and Martin-Löf, verificationism serves as the backbone to modern intuitionistic and constructive meaning theory.

Room and board for a year at UC Berkeley is $14,388. That's for nine months (June, July & August you have to vacate, IIRC). So, that's about $1,600 per month.

On the other hand, I lived in a fairly spacious apartment with one flat-mate; my half of the rent was $700. I don't remember how much I spent on food, but it was probably around $200 per month; utilities another $100. The apartment was a 20 minute walk from campus.

So, off campus expenses for a living far more comfortable than cramped dorm life was about $1000 per month.

Over the course of the three years it took me to complete my degree, that means I saved about $16,200 ($600 saved per month, 9 months per year, for three years). [That's "thousands and thousands".]

At many colleges, it is way cheaper to stay in an big apartment than in a cramped dorm. At Berkeley, I saved thousands and thousands of dollars by living off campus in a pretty big apartment with a "flatmate" but not a "roommate".

"sumeria"? think it's called "sumer"

I translated this recipe back while I was in school! Lots of fun.