Hacker News: xavxav

New comment by xavxav in "Flash-KMeans: Fast and Memory-Efficient Exact K-Means"

xavxav — Fri, 20 Mar 2026 12:19:11 +0000

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.

Software Archeology in 2026

xavxav — Mon, 16 Feb 2026 21:46:52 +0000

Article URL: https://xav.io/blog/software-archeology/

Comments URL: https://news.ycombinator.com/item?id=47040761

Points: 2

# Comments: 0

New comment by xavxav in "Inflatable Space Stations"

xavxav — Tue, 25 Nov 2025 20:39:35 +0000

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

New comment by xavxav in "Breakthrough in antimatter production"

xavxav — Mon, 24 Nov 2025 09:32:11 +0000

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

New comment by xavxav in "MinIO stops distributing free Docker images"

xavxav — Wed, 22 Oct 2025 10:44:49 +0000

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.

New comment by xavxav in "Slack has raised our charges by $195k per year"

xavxav — Thu, 18 Sep 2025 08:08:10 +0000

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?

New comment by xavxav in "Whisky is no longer actively maintained"

xavxav — Wed, 09 Apr 2025 13:38:38 +0000

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.

New comment by xavxav in "Alphabet spins out Taara – Internet over lasers"

xavxav — Mon, 17 Mar 2025 23:15:59 +0000

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

New comment by xavxav in "Serialization Is the Secret"

xavxav — Thu, 03 Oct 2024 09:44:51 +0000

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.

New comment by xavxav in "Serialization Is the Secret"

xavxav — Wed, 02 Oct 2024 12:21:44 +0000

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

New comment by xavxav in "Rewriting Rust: A Response"

xavxav — Fri, 27 Sep 2024 18:29:33 +0000

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

New comment by xavxav in "We built the city of Colombo in Cities:Skylines"

xavxav — Wed, 04 Sep 2024 08:46:10 +0000

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

New comment by xavxav in "A high energy hadron collider on the Moon"

xavxav — Sun, 11 Aug 2024 14:32:10 +0000

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.

New comment by xavxav in "A high energy hadron collider on the Moon"

xavxav — Sun, 11 Aug 2024 14:29:13 +0000

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

New comment by xavxav in "Ask HN: What's Prolog like in 2024?"

xavxav — Thu, 18 Jul 2024 11:50:56 +0000

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.

New comment by xavxav in "Zed on Linux Is Here"

xavxav — Thu, 11 Jul 2024 08:59:31 +0000

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.

New comment by xavxav in "Formal methods: Just good engineering practice?"

xavxav — Mon, 24 Jun 2024 09:49:13 +0000

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.

New comment by xavxav in "Diffusion on syntax trees for program synthesis"

xavxav — Tue, 04 Jun 2024 17:37:50 +0000

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

New comment by xavxav in "A breakthrough towards the Riemann hypothesis"

xavxav — Tue, 04 Jun 2024 17:32:47 +0000

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

Visions of the future: formal verification in Rust

xavxav — Wed, 22 May 2024 15:40:49 +0000

Article URL: https://xav.io/blog/rust-formal-verification/

Comments URL: https://news.ycombinator.com/item?id=40442330

Points: 3

# Comments: 0