xavxav

37 ms·

1.
by xavxav 6mo ago
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.
2.
Software Archeology in 2026(xav.io)
2 points by xavxav 7mo ago|0 comments
3.
by xavxav 10mo ago
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 robust
4.
by xavxav 10mo ago
you just need to speed up in the opposite direction by flipping around and firing bombs on the other side.
5.
by xavxav 11mo ago
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.
6.
by xavxav 1y ago
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?
7.
by xavxav 1y ago
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.
8.
by xavxav 2y ago
basically every european country? they've all had much larger datacaps than north america for years preceding 5g and most are quite densely inhabited.
9.
by xavxav 2y ago
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.
10.
by xavxav 2y ago
What do you mean? let-bindings don't interfere with referential transparency. `let x = 1 in let x = 2 in foo` is referentially transparent.
11.
by xavxav 2y ago
> * "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
12.
by xavxav 2y ago
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,
13.
by xavxav 2y ago
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
14.
by xavxav 2y ago
It's only ~400 times the circumference of the LHC so that seems like a pretty good increase.
15.
by xavxav 2y ago
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 predictabil
16.
by xavxav 2y ago
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 quickp
17.
by xavxav 2y ago
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 inte
18.
by xavxav 2y ago
> 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
19.
by xavxav 2y ago
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
20.
Visions of the future: formal verification in Rust(xav.io)
3 points by xavxav 2y ago|0 comments
21.
by xavxav 2y ago
hey! I'm the author of Creusot, happy to answer any questions.
22.
by xavxav 2y ago
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
23.
by xavxav 2y ago
> 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 fa
24.
by xavxav 2y ago
> 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
25.
by xavxav 2y ago
> 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
26.
by xavxav 2y ago
Can you compare how your approach contrasts to Aeneas or RustHornBelt? How do you handle pointers and mutable borrows?
27.
by xavxav 2y ago
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 wa
28.
by xavxav 2y ago
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, especia
29.
by xavxav 3y ago
> 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 be
30.
by xavxav 3y ago
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 s

More ›