alethic

Joined 1 year ago

Karma

Submissions

Member since

Aug 30

Recent submissions

Unfortunately, a large proportion of stories submitted to Lobste.rs are slopped out... even if they don't mention AI, it's hard to escape there. Hacker News at least has functioning story-level moderation.

Comment · 18 days ago

Ah yes, separate software processes is probably the confusion here. Avoiding certain classes of deadlocks and hangs is also something that's not particularly guaranteed by imperative programs. You can throw a type system on it and get some of them (session types I think are quite expressive), but in practice I don't know of any imperative languages with a type system rich enough to do this.

Comment · 19 days ago

... in what regard?

Comment · 19 days ago

Not well. Xiaomi published a detailed report of their RL process for their recent MiMo v2.6 model (https://news.ycombinator.com/item?id=49792730), which I read through recently. It is an interesting insight into how constructing RL environments work -- for some things, like code generation or code exploitation, there are naturally-perfect RL environments (Github issues + the closing PRs for the former, CVE databases + getting smaller language models to generate exploits triggering them for the latter) -- but for some other things, like code /quality/, Xiaomi at least (and presumably Anthropic et al.) simply do not have any objective criteria.

So they generate a code "rubric" and give a model some number of gold stars for how "well" another language model thinks it satisfies specific enumerated aspects (for code, this is gonna be things like using language features idiomatically, compactness, etc; for writing, this is gonna be things like what you'd get graded on in writing assignments in the fifth grade). Incredibly stupid. I'm shocked it works at /all/. But the lack of any truly objective criteria of "quality" wrt. code/prose explains why it doesn't work all too well, IMO.

Comment · 19 days ago

Choreographic programming is well-known within the programming languages literature, which is the audience this README is intended for. The level of detail here is fine, not everything is written with being posted on news.ycombinator.com in mind.

To explain it briefly though, choreographic programming is a method of writing distributed programs that communicate in some message-passing fashion by -- rather than writing separate programs that communicate with send/recv and must be very intentionally designed to be in sync -- you have /one/ unified messaging primitive. In a typical distributed system, you might have something like A.send_to(B) / B.recv_from(A). In a choreographic system, you'd rather have something like A ~> B, where send_to and recv_from are /projected/ from ~> into separate programs during the process of compilation.

You might want this kind of abstraction for various reasons, but the biggest is that many choreographic systems offer a guarantee of deadlock-freedom. This isn't without tradeoff. At the moment, choreographic systems (and session types, another distributed abstraction) are very bad at handling any kind of failure / degraded performance over the network. There is active work within the PL community on resolving these issues, but for now, choreographic programming is primarily useful for prototypes, rather than production systems.

Comment · 23 days ago

Haha, that is a funny sentiment to express :-D

I agree though! I think their website has been influenced by and has influenced various Japanese-language sites in my bookmarks. It is a very rectangular style.

Comment · 1 month ago

I am incredibly excited for this -- while I love doing StreetComplete quests myself, the lack of iOS support has prevented me from grabbing my friends / random strangers and turning mapping my city into a social outing. I'm going to wait until it's officially available, but this is so wonderful... gosh, I can't wait. First style of quest I'm going to get ppl coordinated with is accurate hours on local businesses :^)

Comment · 1 month ago

There was a long-running data corruption issue with non-raw sends that was finally found and patched in 2025: https://github.com/openzfs/openzfs-docs/issues/494. But I agree, it's about as safe as they come. I trust it far more than any other file system, in large part due to all its built-in redundancy and the way it makes backups trivial (encrypted sends <3)...

Comment · 2 months ago

Racket and Rhombus are nice for writing embedded DSLs, yeah. More generally, they're nice for writing macros. Scheme in general is nice for writing macros with its `syntax-case` and first-class notions of syntax objects, but Racket is /really/ nice with its `syntax-parse` and explicit notions of phase levels... If you are interested in learning, Greg Hendershott's "Fear of Macros" is often recommended as a good introduction. https://www.greghendershott.com/fear-of-macros/

Comment · 2 months ago

Cool project! The title is not quite accurate though, the project is "a metadata search engine similar to searxng in rust". It doesn't look like it implements / intends to implement any of SearXNG's advanced features, like weighting of individual sites in results, wikidata integration, or... a frontend :-)

Comment · 2 months ago

No, they do a pretty good job at getting around it. I only run into issues with Brave/Startpage, Google/DuckDuckGo/Wikipedia all work fine. And when you're fusing together multiple sources getting CAPTCHA'd is not actually a big issue, it's more so a thing to fix later.

I would say also -- if search engines are making you do CAPTCHAs every few searches, this is probably an issue with your exit node. I notice a sizable increase in CAPTCHA barriers when I'm on my VPN (most annoyingly Google/YouTube, which sometimes will serve you an infinite number of CAPTCHAs w/o letting you through).

By contrast, my SearXNG instance is making ~100 searches a day from a known good IP address (being my VPS), so rate limiting is less of a problem. You can also set up API keys for many search engines.

Comment · 3 months ago

(I should note that there is also utility in confirming the correctness of results that are too complex to be adequately verified by humans. The recent result that NF is consistent wrt. ZFC, among others (Peter Scholze's Liquid Tensors project) are examples of this. But that's distinct from "autoformalization" as commonly applied.)

Comment · 3 months ago

The utility of autoformalization is not actually in confirming the correctness of human-checked results. Mathematicians have a pretty good peer review process. I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect -- though I'm sure cases exist, it's astoundingly rare.

The mathematics community's motivation for formalizing problems like Maryna Viazovska's sphere packing results in Lean weren't because the results were in doubt -- she won a Fields Medal for it, it's an extremely examined proof -- but because formalizing those results would lead to a lot of interesting and useful mathematical objects needing to be formalized as a prerequisite, which could then be merged into Lean's Mathlib and become useful for anyone working with Lean, particularly students. Having a library of idiomatic proofs available in a formal system capable of checking your work is Really Cool! Working in a proof assistant is a great way to develop mathematical maturity, especially for people who might not have an undergraduate education available to them.

(Unfortunately in the sphere packing case, the research group working on it made the mistake of trusting one of the various "AI for Math" slop companies, who promptly rugpulled them: https://arxiv.org/html/2603.03684v3)

So the short answer is "it depends on what you want". Lean is an eminently usable system for humans and LLMs alike; Metamath is uh. Not. But yes, Metamath seems to have a more trustable kernel wrt. the independent verifiers, so if that's all you're after it would be a better pick. But... there's only so many bugs Lean's kernel can have. At some point, they'll all be found.

Comment · 3 months ago

This is of course a massive privacy violation, since the code that scans for CSAM can be switched out to scan for anything else at any time. (It's even easier to do now than when Apple first proposed it, as language models since have gotten good at reading images.)