Viewing profile — 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 spar…

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)…

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 t…

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 …

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 ca…

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 …

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…

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…

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 trad…

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…

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 slowdo…

> 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 i…

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…

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 b…

> 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 mutabi…

> 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 fu…

> 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 funct…