Jason (jcreed) wrote,
Jason
jcreed

Print them out now, and squirrel them away

There are two kinds of ways ideas can work out, and in both it is like you are pounding the idea with a hammer by thinking about it. In the one case, it is like a fragile piece of pottery that crumbles to bits, because you just hit it with a hammer. I often have these ideas, and fear thinking about them too hard, often doing so just before my advisor meeting out of guilt, finding out they don't work at all. In the other case, it is a sturdy piece of metal fresh from the fire, and hitting it in just the right way actually makes it take a better form than it did when you first had it. So far, knock on wood, this idea I had (of isolating resource use by sort of imitating what CLF does except the type operator I have is parametrized over worlds, and not quite exactly a monad, thereby giving the logical-framework user a way to predicatively and explicitly quantify over resource expressions rather than entire contexts) seems to be the good kind.

I went to a talk by John Reynolds, which was associated with him receiving an award named after Dana Scott. Given that they are already well-known superstars in our department here, the whole business seemed rather self-congratulatory, but I'll be damned if Bob Harper didn't give one of the most stirring "here I am introducing the guy who's introducing the guy" talks I've ever heard. (Although he talks so fast it's kind of like he's a robot who learned to perfectly imitate human speech...) Awards seem hollow until you realize just how much amazing work these folks have done, and how much they all mutually owe each other in terms of productive collaboration.

John in particular has this reputation for always being 30 years ahead of his time — there are untold numbers of CS research paper bibliographies that go like So & So 95', Wossface et al. '98, Reynolds '79 — so Dana asked jokingly after John's talk how we're supposed to find his current notes 30 years from now. The title of this entry was his answer.
Tags: talks, work
Subscribe

  • (no subject)

    K's off at an atypically Saturdayish Type-Thursday event, so I stuck around the apartment hiding from 100-degree heat, and noodled around with…

  • (no subject)

    Playing around with the agda javascript backend, now. Like, my ears are popping from the sudden change of type-theory-pressure.

  • (no subject)

    https://deadlockempire.github.io is a very cute edutainment game, meant to teach people about deadlocks and race conditions and concurrency…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    switch
    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    Help
  • 6 comments