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

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.