xavxav

search trees tend not to scale well to higher dimensions though, right?

from what I've seen I had the impression that Yinyang k-means was the best way to take advantage of the sparsity.

aren't rockets like the starship almost the opposite of what you want in a space station? They want to minimize the integrity of the rocket as much as possible (without blowing up) to reduce the mass while for a station you want robustness (for pressure & impacts).

you just need to speed up in the opposite direction by flipping around and firing bombs on the other side.

garage devs have told me of 10PiB+ deployments in production, but I've never operated one at that scale so I can't share much insight into the experience. Probably best to ask on their matrix chat.

I'm surprised GDPR has nothing to say about this. You should have the right to your data, but I suppose that doesn't extend to companies?

That's unfortunate, I really preferred Whisky to crossover purely for the UX, I would happily pay for a crossover license if i got to keep the whisky app itself, crossover's ui is archaic and ugly in comparison.

basically every european country? they've all had much larger datacaps than north america for years preceding 5g and most are quite densely inhabited.

Sure, scopes are not as easily syntactically visible, but each assignment is creating a new scope, that doesn't change anything for equational reasoning which has to account for captures / substitutions anyways.

What do you mean? let-bindings don't interfere with referential transparency. `let x = 1 in let x = 2 in foo` is referentially transparent.

* "As provable as Ada/SPARK": I'll let you read the design in [2] and decide for yourself. But Yao will also have contracts.

Without being too self-indulgent, I'm not sure there is that big of a gap between the two in provability, there are now a huge array of verifiers for Rust code which are being used to verify real code: SAT/SMT solvers, kernels, memory allocators etc...

Not really, conceptually it probably shares a lot of the same foundations that a useful simulator would have, but its important to keep in mind that they aren't actually simulators of cities in a realistic sense.

Games such as cities, inherently embed a view of how the "right" city would be organized, providing tools and incentives to nudge you in that direction. Consider how all social problems can be solved by simply plopping down the relevant class of building nearby. Or simply the absence of parking lots!

There's this old article on the subject: https://www.polygon.com/videos/2021/4/1/22352583/simcity-hid...

1. the article explains how many materials could potentially be sourced on the moon and provides potential magnet compositions to address that as well. 2. The moon weighs ~8.1 x 10^19 tons, if we use their iron based magnet design and ship everything from the earth (iron is present on the moon), it would require ~1 million tons aka 10^6 tons or approximately 0% of the weight of the moon. 3. See above.

It's only ~400 times the circumference of the LHC so that seems like a pretty good increase.

There is still academic work on Prolog, and more broadly deductive / logic programming. If you are looking at things with a more industrial bent, I would look to Datalog which trades generality in Prolog for performance and predictability. Alternatively, you can go the other way and look at lambdaProlog which adds real abstractions / HOFs to Prolog.

What I've seen in practice is that while Prolog may be good at describing a solution, its performance is often too lackluster and brittle for actual deployment: it probably fits more as a prototyping language before you do a classic implementation of the solution in a more traditional language.

I did the same thing, with the same limitations for years, but I've transitioned to using the tiny package `DailyOrganizer` which can create a note for each day, along with a small custom command to open my note directory in the quickpick (to browse old notes). Having this has meant that I just throw notes down, maybe I forget them maybe not, but it at least they'll be saved properly.

I'm a researcher in formal verification; my thesis was building a tool to do this kind of stuff and I agree with the grandparent (though I would say probably closer to 5-10x slowdown not 100x).

Proofs are hard and often not for interesting reasons; its stuff like proving that you won't overflow a 2^64 counter which you only increment (aka something which won't happen for another couple billion years).

Current tools are only useful for specific kinds of problems in specific domains; things where a life really depends on correctness. Outside of those cases, lightweight techniques provide much more bang for your buck imo.

After decades of compiler research and super compilers chugging away, we're sort of at a point where discovering novel optimizations with results that are more than a smidge of improvement is almost impossibly unlikely. Compilers today are really good.

I agree when it comes to peephole optimizations, but there's still a lot of juice left in exploiting language guarantees (immutability, non-aliasing, data-parallelism), however most compiler developer energy is spent propping up C/C++ and consequently optimizations are developed with those languages in mind.

Indeed, the first incompleteness theorem tells us that any logical framework which can express Peano arithmetic must necessarily contain true (resp. false) facts for which no (resp. counter) proof can be given.

Sometimes you can prove that no proof exists about a specific sentence (that's what his incompleteness proof does), and I think you could extend this technique to construct sentences where no proof exists of whether it has a proof, etc...

hey! I'm the author of Creusot, happy to answer any questions.

I would assume its not 'safety critical' but 'business critical', disabling GPS would mean slowing down departures / arrivals which means the airport losing money. I recall there being a similar issue with Lufthansa and SFO causing planes to get rerouted to oakland.

I guess that immutable Rust is simpler to verify with the other systems too.

I don't think that's the case (it's not harder either). The type system of Rust makes handling mutability fairly trivial in verification, in fact it could be translated to immutable code in a continuation monad like the Tardis monad from Haskell I think.

Could you sketch in a few bullet point what you think is missing and how to fix the gaps?

Not yet, I am planning on writing some blog posts about it but there are still enough fuzzy points I don't want to share yet.

... since the proliferate transitively along the control flow graphs. ... suffer from the same cancerous growth.

This is one of the biggest and most difficult issues of verification, I fully agree. The 'promise' of verified code is that you don't need to understand the code, you can just look at the smaller, higher-level spec, but right now verified code has a specification & proof overhead > 1, it needs to drop to < 0.1 for it to become economical.

You can knock off most things you have to prove with a SAT solver. But you'll need something heavier for the hard problems. Coq is too manual. The author thinks ACL2 is too functional. Not sure what to do there, but I've been out of this for decades.

Agreed, though I think Lean is making big progress in the UX front of ITP verification through its extensive meta-programming facilities.

My issue with these tools applied to verifying external languages like Rust, is that the proof is not written in the target language, forcing your developers to learn two languages.

I have recently been thinking about what a "verification aware Rust" would look like, colored by my experience writing Creusot, the work on Verus and Aeneas and my time in the lab developing Why3. I think building such a language from the ground up could provide a step change in ease of verification even from Rust, particularly with regard to those "hard parts" of the proof.

Can you compare how your approach contrasts to Aeneas or RustHornBelt? How do you handle pointers and mutable borrows?

These are all valid points, I also very annoyed at noisy home appliances (fridges...), but I'm always shocked by how loud it is as soon as you step outside. I remember during the first lockdown I would take walks out in Paris and it was so quiet and peaceful; the sheer quantity of decibels originating from motorized vehicles is insane.

My understanding is that they've more or less always done this for various reasons: security patches, compatibility, dependency versioning. I understand the historical reasons that led to this structure for package management, especially with how brittle C dependencies seem to be, but I truly hate this practice. It seems to make it exceptionally difficult for authors of major software to establish any sort of invariants or security boundaries.

health emergencies

We have socialized health care, and even private care is like 1% the cost of american healthcare. I got elective surgery without insurance which included full anethesia in a private clinic and they were very sorry because the total would be 600 euros.

retirement

Public retirement is ~50% of your average lifetime salary though the age was recently raised from 62 to 64 (in the face of massive protests).

losing a job

Firing is harder to do in the first case, they have to have cause, or the company has to be facing bankruptcy, there's a long notice period. Unemployment is also a decent percentage of your salary and can go on for months.

Frankly on 60k a year, you live well even in a city like Paris, you're not living a life of luxury but that's comfortable upper middle class levels (in Paris).

Another key factor: NASA has no control over its funding (and thus vision) it’s at the mercy of congress each year which makes planning and financing large projects hard. They have projects and designs imposed from above regardless of the scientific or engineering benefit.

I'm not familiar with the structure of stream payouts on Spotify, but if 80 million streams gives 12 dollars, that means Taylor Swift's 26.1B streams give ~4k?

I knew the rates were bad but damn...

A blockchain provides nothing of value here, what you need is a mechanized proof, and once you have that the blockchain in no way contributes to the trust.

The trust in a Coq proof comes down to "do you believe that the 8kloc kernel faithfully implements CiC+extensions and is this metatheory a sound type system?". As it is today, anyone could claim or commit a proof bounty by posting a Coq / Lean file / project online, all that's required is an email.