jmgrosen

hope to get a greg collab on here sometime

Even at 23mph, a pedestrian's chance of death in a collision, in the US over the years 1994-1998, was only 10%: https://aaafoundation.org/impact-speed-pedestrians-risk-seve...

I don't mean to imply that that is a low risk, only that speed is quite a crucial factor.

Especially the Field model!

given the crackpot proofs received by coq-club, i imagine it would indeed

are there any documented cases of this actually happening in the wild?

Thank you for the self-promotion, Scheme for Max looks like something I’ve been wishing for for a long time!

Use an existential type, usually called Some in Haskell: https://hackage.haskell.org/package/some-1.0.5/docs/Data-Som... The implementation of this type one has in their head (a GADT) adds a boxing overhead, but the actual implementation in this library uses a newtype.

That way if you have a type Expr a, you can have a list type [Some Expr].

yes: https://dspace.mit.edu/bitstream/handle/1721.1/130136/The%20...

(sorry for lack of details in my post, on mobile)

No, it’s not—-they’re passing in a “node”, not a list, which always contains both a head element and a (nullable) tail pointer. That’s why it can’t separate the head in the case of size one: the node must maintain a non-null head.

Some of you may enjoy this fantastic recent paper on how to win both the comprehension benefits of splitting lexer and parser AND the performance benefits of fusing them: https://www.cl.cam.ac.uk/~jdy22/papers/flap-a-deterministic-...

This is absolutely ridiculous. I love it.

I think more like 5.5 minutes: https://www.wolframalpha.com/input?i=300+nautical+miles+%2F+...

The second page starts the "FULL PRESCRIBING INFORMATION"; the body weight quote above comes from section 12.3 of it and there is no mention of a weight exclusion in the discussion of the clinical studies in section 14. AFAIK, "label" typically refers to this sort of ~20 page prescribing information, but is there a different label you have in mind? I believe the one-page package insert is the last page, page 17.

Very cool!

Just a random thing I noticed reading through [1]: you might have a bug in how you calculate the magnitudes of the signals? When you assign the output of the low-pass filters on the high frequency to the input of the magnitude approximator, you assign the imaginary LPF to the imaginary input but the real LPF to also the imaginary input, which I think is incorrect? Since I’m on mobile, it’s easiest for me to show sign a screenshot: https://i.imgur.com/tAQe5Sr.jpg (If that is indeed a bug, I’m curious how that might impact the results!)

Not sure whether I'd prefer to be Bond, or a pirate: archery, fencing, pistol, and sailing.

I worked the polls in Allegheny, and while the broad strokes are similar to what you described, there are definitely a few differences:

- Most people fill out their ballot on paper with a pen, but a voting machine is also available to generate a ballot (anyone can request to use the machine, but it's intended for those with disabilities). Either way, the voter then feeds their paper ballot into a central counting machine (most districts only have one, but some have more).

- Police are in no way involved (unless the poll workers call them to attempt to address an issue during the day). The judge of elections is responsible for picking up the materials a few days beforehand and then dropping them off at the county office at the end of the day.

- Only four receipts are printed: one to go to the county office, one stays with the minority inspector for a year, one is posted outside the polling place, and... I can't remember what happens with the fourth.

In any case, though, thanks for writing this up in detail -- it's good to read how other places do it, and for those that haven't been a poll worker, it's good to read how at least one place does it!

It appears so! https://github.com/ms-jpq/gay/blob/95129960bc94f017648b93944...

Well, I will defer to your judgment! I’m by no means a type theory person.

My understanding was that these features are how quotients are managed to be implemented. But perhaps that is wrong.

My understanding is that this shows how vanilla Coq still can’t encode quotients well. This project relies on a PR [0] that breaks term normalization, which makes it highly unlikely it will be merged. My understanding is that Lean’s implementation of quotients also breaks normalization, but they don’t care as much about that as Coq devs do.

[0]: https://github.com/coq/coq/pull/10390#issuecomment-554316311

It does say that multiple times:

> It is believed that some of the crowd control devices are capable of emitting electric shocks in a bid to neutralise any perceived threat...

> The control weapons, which potentially have the ability to shock people, have been part of the training...

> Amnesty added that it has information that more than 200 shock capturing forks were sold to the Linhe District Public Security Bureau back in 2014.

The wonders of Unicode: "Superscript One" has codepoint U+00B9.

It all seems very fast for me. I also see no problems with hint databases... maybe check the JS console for errors?

Well, perhaps they should upgrade it for the sake of the ~170 CVEs that have been published against Java 1.8.0_60? https://www.cvedetails.com/vulnerability-list.php?vendor_id=...

Sure, a lot of those probably don't apply to how they're using Java, but I'd bet at least a couple do.

Don't forget building 18! 54 on its side :)

Earth Day hack, from last year: http://hacks.mit.edu/Hacks/by_year/2017/earth_day/ was left up for several days (not listed there, but I was around to see it up)

I don’t think that sort of hack would have been taken down any less quickly in the past. The only time dome hacks have lasted a while have been when they’re extremely tricky to take down.

I have some further opinions about what you allude to at the end of your comment, but that should probably be taken offline.

I’d have disagree. Have you seen Hackapult? http://hacks.mit.edu/Hacks/by_year/2015/hackapult/

There are fewer hacks nowadays, and they’re usually less ambitious, but I would argue it’s for reasons other than hostility from the Institute.