the_french

I've talked to Yannick quite a lot in the past as my lab develops Why3 and SPARK uses my translation for their new support for pointers (access types).

Additionally, my advisor collaborates with them on counterexample generation, especially with managing to get readable counterexamples out from the SMT. We've toyed a little with invariant generation but its very tricky to get something actually usable. Additionally, I have the personal (soft) requirement that the generated invariant should be injected into the source code and not purely internal / hidden.

That kind of software is not usually written in Rust (or Ada), but using Simulink / SCADE or other model-based and synchronous tools, afaik.

> 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.