"Interactive Theorem Proving and Program Development: Coq'art: The Calculus of Inductive Constructions", and it's kicking my ass to a humbling degree. I'm spending, conservatively, 15 minutes per page, in chapter /one/. I don't know if I'm dumber since I was in undergrad, or if this is my true info onboarding rate and I did undergrad wrong, or what, but this isn't boosting my ego at frigging all.
This is very cool forum site, kudos to Zorba et al for their hard work and a smoothish launch.
In the vein of navigating through read comments to new ones, it would be cool to be able to see how many unread comments a collapsed comment has beneath it. Maybe this could be pushed to user-side logic? How does the unread-comment counter work for the thread index page?
- Prev
- Next

Ethics question: how evil would it be to develop a payload for a mechanically suitable off-the-shelf remote-control multirotor drone that would enable a remote user to pierce a car or truck tire and render it irreparably leaky?
For numbers, let's say:
the drone is viably controllable up to a quarter-mile from an off-the-shelf controller station (read: phone or lap, maybe with a radio dongle)
the drone is not autonomous outside basic flight stability and safety features to other humans, so it has to be guided to a tire and the knife triggered by the user
the knife can be triggered 4 times per flight
the drone's battery and knife can be replenished within a minute by the user
the knife is captive, so it can't hurt anything the drone isn't immediately adjacent to, and magically can't be modified to do otherwise by end users.
the drone and ground station are readily replaceable for <$10K, so accessible for a small organization or an org with donors, but not a typical individual.
This is prompted by my trying to inhabit the viewpoint of modern dirtbag left activists, such as those who protest by gluing themselves to roads and suchlike.
Factors I can think of offhand:
This enables grassroots enforcement of no-car, no-truck zones for the anarchistically-inclined
This makes destruction of property safer for the perpetrator
This enables wider-scale destruction of property viable for a single user
The payload designer isn't hard to replace, since the payload is easy to design, but the payload only needs to be designed once and then plans distributed
Obviously, this makes hit-and-run violence easier and safer, but that rate is already low and dropping, but maybe someone out there is only held back from a spree by having to be present for the attacks in person? If so, why aren't they a sniper on a spree already?
Once the payload is built, how much harder is making the entire thing autonomous? To the degree of "here's a car-shaped thing, slice the tires"? "Here's a geofenced area, slice the tires of all car-shaped things in it"? "Here's a geofenced area, slice the tires of all cars without a badge"?
More options
Context Copy link