the_french

> But we know how that goes and nobody actually will care about the scooter enough to return or take care of it.

Looking at countries like the Netherlands this is not true. Train stations have rentable bikes which are always available in sufficient quantities.

> So what do we do? Uber-Tesla-Subway pods. I call it by phone, it shows up to my house, either transfers me or lets me dock with the subway and then brings me the last mile just to leave me there for the next thing it has to do.

Individual 'pods' will just never be a sufficiently scalable & ecologically friendly solution for any real city. There's just no way that having several hundred kilos of metal & plastic per individual, along with the space requirements (esp for safety) works.

On the other hand, autonomous & shared 'cars' could replace individual vehicles for hauling / transporting as peak usage would be much lower than for transit.

no, it isn't. Don't go around spreading FUD, the article makes no mention of causation for the deaths, extrapolating that to an entirely hypothetical (and unfounded) vaccine induced immunodeficiency is unjustified.

GDPR fines can go up to 4% of global revenue so the 62 cent comparison seems apt.

if I recall correctly, the fine scales up as time goes on up some (2?) percentage of company revenue. Like most people I would be happier seeing them get a several billion dollar fine right off the bat but so long as it eventually becomes unbearable that's good enough for me.

I don’t think most theoretical physicists are seeking wealth, they tend to have deeper intellectual motivations.

This is an interesting idea but is there any description of the soundness of this approach? Any functionality capable of subsuming not just inductive types but higher-inductive types is going to be very subtle. I looked around on the repository but I can't find any formal description of the language or type theory, which is worrying for a proof tool.

> Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs.

Nitpick, because those programs have no type they are not members of the Simply Typed Lambda Calculus but only of the underlying untyped calculus

The french government has actively promoted the growth of forests / their management for over a century. Today, there are more acres of forests than at the turn of the twentieth century for example.

from the cursory read of the documentation on the openbsd site it doesn't seem to support TPMs. Setting up the encryption of a disk paritition does seem easier though.

On some fronts it even feels like things have regressed. Trying to resize an encrypted partition is way, way too difficult. And it seems like GParted doesn't handle LUKS so you're back to manually typing block offsets on the command line.

If you wanted to use a TPM to store the FDE passphrase, well, you have the patience of a saint. Compare this to Mac or Windows where you click a single button and it's all setup, including TPM!

As much as I love linux for server environments, it remains a failure when it comes to modern desktop environments.

This may be rather naive but wouldn't using an energy storage mechanism for structural purposes be a bad idea?

That could mean that every fender bender now risks igniting the hood of your car.

a law which was democratically approved, with public oversight, a mechanism for undoing it and not at the whim of private shareholders.

I think that building a competitor on top of facebook is against their terms of service. You wouldn't be able to build an 'alternative facebook client', legally at least.

This approach ignores all the aspects that made whatsapp / chat services popular in the first place. A short list:

  - Contact Discovery
  - Group chats
  - History / Log
  - Shared message order
  - Communication beyond text (emojis / reactions / inline images) 
  - Ability to receive messages while offline 
  - No need for technical skills

These aren't trivial features, they are prerequisites for any replacement, decentralized or otherwise. Just because we as developers like / tolerate things like IRC doesn't mean the rest of the world will accept it.

The vast majority of cars in the streets of paris are not from suburban commuters but from people in the 15th and 16th (read: wealthy) neighborhoods preferring to drive than to mingle with the rest.

Besides, removing cars from the road means that busses will be more reliable (less traffic jams) so you can avoid the trains in more situations.

I think it's misleading to say ITERs technology is 30 years behind. A lot of the tech that has been going into the ITER design didn't exist 30 years ago! They didn't anticipate developments in super conductors but this is by no means a 90s machine built 30 years too late.

Part of the role of ITER was to fund the research to develop the reactor's components while giving everyone a concrete goal to work towards. The challenge with ITER is much more than construction.

It's a design we've modelled and predicted should work. Since we've never actually built anything close to it, we have no way of knowing whether those models were even close. If ITER shows results that are even close to breakeven you can expect a rush of newer designs using technological advances to shrink scale and improve performance.

Besides, ITER is also meant to help develop experience in handling large plasmas for extended periods of time, that knowledge will transfer to other designs.

the yt recommendation algorithm is probably the worst among all the major platforms. It will pigeonhole you into the same 10 videos, which you will never escape. I listen to music on youtube relatively frequently but then it will always go back to the same 10 songs its decided i should listen to, no matter what genres I play.

Part of that pressure comes from the lack of funding though. When you have to fight against 100 other applications for a grant showing you have a recent track record of well-cited papers helps you stand out.

If researchers had steadier access to funding there would be less pressure to constantly publish 'breakthroughs' to secure next years funding.

I think you would be interested in Noether, a full language design based around this principle: https://tahoe-lafs.org/~davidsarah/noether-friam4.pdf. I've always been sad that an implementation was never created. It's one of the most unique designs for a language in the past decade.

I honestly have never wanted to receive mail from anyone other than a real human being. There is not a single 'account update' or marketing mail, etc.. that I am happy to see, nor has there ever been.

Does anyone actually enjoy those mails? How is it any better than the classic physical letterbox spam that used to be more common?

I think replicating RoR in Haskell is explicitly the goal of IHP.

I don't have a problem with them making opinionated choices for projects, I really don't want to have to wade through library choices and configuration each time I start a project.

Granted I started out as a Rails dev...

I'm starting my PhD under the supervision of one of the Frama-C authors, if you have questions I can relay them.

In general I've found deductive verification techniques interesting / promising because they free engineers of a lot of required but tedious details you'd have in ITPs.

However, I think there's a LOT of room for improvement in terms of ergonomics of proof debugging. For a frequent (for me) problem when debugging invariants is conditionals that break the invariant.

if i have some code doing something like

    while (X) {
      invariant { forall i. 0 <= i < N .... }
      if j < i A else B 
    }

But it turns out that one of the branches A, B doesn't preserve the invariant well all the provers will tell me is 'can't prove this!' it's up to you to perform the transformations that split the two cases (granted in this example it's trivial) so that you can see that only _one_ branch was failing.

I think that there should be transforms that automatically do things like split the range of an interval along relevant points (aka j) to help you figure out which portions are failing.

There are tons of other issues related to proof ergonomics that could be improved, the UIs are really stuck in the 90s!

Is there a tool that works for the limited subset of PDFs generated by Latex? Do those documents have more structure than the average PDF? Less? It'd be nice to extract text from scientific articles at least.

The city / region has been working on that by decentralizing major government and business institutions. By pushing them out of the core in to neighboring suburbs it allows those employees a real chance at living near work in more than 15m2.

At the end of the day the only real solution to commutes / crowding is going to be spreading the load out on more communes and cities.

Even worse, a major French bank removed their perfectly fine password requirements and replaced it with a 6 digit PIN that you have to enter via an on-screen numpad. They explicitly block password managers from autofilling too! And I had just managed to get my parents to start using one.

Its no huge surprise that spreadsheets implement a form of FRP . Specifically, you can look at loeb's function [1] as an example of the relation. Being able to focus on the data itself while easily composing operations is definitely functional in nature.

However, FP is not a silver bullet either. In practice I think humans care a bit less about correctness than compilers and would like some aspects of the language to be 'fuzzy' for lack of a better word. To most people "1" and 1 are the same thing so why shouldn't the compiler understand that. There could be potential for a dynamic-fp language of sorts.

[1] http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet...

In the same vein what would happen if Apple decided to destroy their master key and all backups? While that would completely screw over iphone updates I would honestly prefer that to the FBI getting source and signing capabilities. If Apple turns over their source it is only a matter of weeks before it gets leaked and its game over afterwards.

Is there anyway to achieve something similar to Quicktime? Or is that what you mean by a 'dark' titlebar? I'd love if the titlebar would fade away when not mousing over it.

I've never had to produce soap even during extended sieges. The only instance it would have helped in was with a FB that had poisonous blood (and killed half my fortress). I always felt that the medical aspects were a bit too easy.