Hacker News: statusfailed

Ral: A shell grounded in programming language theory

statusfailed — Thu, 16 Apr 2026 11:17:26 +0000

Article URL: https://lambdabetaeta.github.io/ral/

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

Points: 3

# Comments: 1

New comment by statusfailed in "Automatic Textbook Formalization"

statusfailed — Sat, 04 Apr 2026 02:39:30 +0000

I am a huge fan of mm0, the thesis[0] is so brilliantly written, and MMC is such a great step towards the kind of verified computing I really want to be doing

[0]: https://digama0.github.io/mm0/thesis.pdf

New comment by statusfailed in "RISC-V Is Sloooow"

statusfailed — Tue, 10 Mar 2026 23:29:45 +0000

The Milk-V Jupiter 2 (coming out in April) is RV23 too

New comment by statusfailed in "Vim-pencil: Rethinking Vim as a tool for writing"

statusfailed — Mon, 16 Feb 2026 13:52:40 +0000

Ahh I thought I was the only one! One line per sentence makes the diffs so much nicer too, maybe we need git hooks to reject multiple sentences per line?

New comment by statusfailed in "Using an engineering notebook"

statusfailed — Thu, 12 Feb 2026 09:54:58 +0000

I didn't find note-taking particularly useful until I started keeping everything in a single notebook with dated pages. This worked a lot better than (for example) trying to organise notes by category - it's often easier to remember when you were working on something than how you categorised it, and once you know roughly when, you can find it by binary search

Explosive GEMM: arbitrarily large FP error can be incurred in the GEMM operation

statusfailed — Mon, 22 Dec 2025 13:07:55 +0000

Article URL: https://github.com/statusfailed/explosive-gemm

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

Points: 1

# Comments: 0

New comment by statusfailed in "The universal weight subspace hypothesis"

statusfailed — Tue, 09 Dec 2025 10:29:04 +0000

I saw a similar (I think!) paper "Grassmannian Optimization Drives Generalization in Overparameterized DNN" at OPT-ML at neurips last week[0]

This is a little outside my area, but I think the relevant part of that abstract is "Gradient-based optimization follows horizontal lifts across low-dimensional subspaces in the Grassmannian Gr(r, p), where r p is the rank of the Hessian at the optimum"

I think this question is super interesting though: why can massively overparametrised models can still generalise?

[0]: https://opt-ml.org/papers/2025/paper90.pdf

New comment by statusfailed in "AI documentation you can talk to, for every repo"

statusfailed — Tue, 11 Nov 2025 10:52:17 +0000

Which repos worked well? I've had the same experience as op- unhelpful diagrams and bad information hierarchy. But I'm curious to see examples of where it's produced good output!

New comment by statusfailed in "Categorical Foundations for Cute Layouts"

statusfailed — Tue, 23 Sep 2025 07:57:23 +0000

Really nice! Had a quick read, here's my quick summary:

- Arrays are typed `S : D` with shape S and strides D

- Each of `S` and `D` is a nested tuple (instead of the flat tuples one typically sees in a tensor framework)

- Together `S` and `D` define the layout of a tensor

- Not every layout is "tractable", but the tractable ones form a nice category

A really good exposition, my only criticism is that it's quite front-heavy- it would be nice to see a detailed example like in 2.3.8 earlier in the document; there is a lot of detail presented early that doesn't seem necessary to understand the core ideas.

Last comment: I suspect there is a connection to strictification[0], would love to know more if the authors see this!

[0]: in the sense i mean here: https://arxiv.org/pdf/2201.11738v3

New comment by statusfailed in "Ask HN: Who is hiring? (August 2025)"

statusfailed — Mon, 04 Aug 2025 09:31:59 +0000

Hellas.AI | Remote | Full Time or Contract | https://hellas.ai

Hellas.AI is building a compiler for categorical deep learning to power decentralised, serverless AI.

We're looking for an experienced Rust engineer. You must have demonstrated:

* Experience in designing and implementing BFT consensus protocols * Ability to engage with academic literature on distributed systems * Understanding of ZK proofs and proof aggregation (you don't need to design these, but you should know how to use them)

Nice-to-have: interest or experience in:

* Deep Learning / ML / AI, GPU programming * Compilers and array programming languages * Category Theory and string diagrams

If you have project(s) demonstrating your experience in one or more of these areas, get in touch!

Our process is simple: we read code you've written and research you've published, then interview you about it. We don't do tedious coding tests.

Email us at hello@hellas.ai

New comment by statusfailed in "Algebraic Semantics for Machine Knitting"

statusfailed — Wed, 23 Apr 2025 12:16:14 +0000

I've been hoping for a nice concrete example of braided monoidal categories for ages, who knew that the best one was string diagrams that represent actual string! Great post!

@the author - I assume you're aware that morphisms in symmetric monoidal categories can be represented using cospans of hypergraphs - do you know if there's a similar combinatorial representation for braided monoidal categories?

New comment by statusfailed in "Catgrad: A categorical deep learning compiler"

statusfailed — Wed, 05 Feb 2025 20:58:38 +0000

(author here) the goals of catgrad are a bit different to JAX - first of all, the "autodiff" algorithm is really a general approach to composing optics, of which autodiff is just a special case. Among other things, this means you can "plug your own language" into the syntax library to get a "free" autodiff algorithm. Second, catgrad itself is more like an IR right now - we're using it at hellas.ai to serve as a serverless runtime for models.

More philosophically, the motto is "write programs as morphisms directly". Rather than writing a term in some type theory which you then (maybe) give a categorical semantics, why not just work directly in a category?

Long term, the goal is to have a compiler which is a stack of categories with functors as compiler passes. The idea being that in contrast to typical compilers where you are "stuck" at a given abstraction level, this would allow you to view your code at various levels of abstractions. So for example, you could write a program, then write an x86-specific optimization for one function which you can then prove correct with respect to the more abstract program specification.

New comment by statusfailed in "Ask HN: Who is hiring? (January 2025)"

statusfailed — Thu, 02 Jan 2025 22:02:10 +0000

Hellas.AI | Remote | Full Time or Contract | https://hellas.ai

Hellas.AI is building a compiler for categorical deep learning to power decentralised, serverless AI. If you're interested in any of the following, get in touch:

* Category Theory and string diagrams

* Compilers and array programming languages

* Deep Learning/ML/AI and/or GPU programming (e.g. CUDA/ WGSL)

* Building and deploying distributed systems

* Peer-to-peer software and blockchain

If you have project(s) demonstrating your experience in one or more of these areas, get in touch!

Our process is simple: we read code you've written and research you've published, then interview you about it. We don't do tedious coding tests.

Some experience of Rust or a functional language (Haskell, OCaml, any Lisp) is preferred.

Email us at hello@hellas.ai

Sled: An Embedded Database in Rust

statusfailed — Fri, 13 Dec 2024 09:54:53 +0000

Article URL: https://github.com/spacejam/sled

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

Points: 2

# Comments: 0

New comment by statusfailed in "Mozilla fixes Firefox zero-day actively exploited in attacks"

statusfailed — Thu, 10 Oct 2024 07:22:26 +0000

Seems bad. "An attacker was able to achieve code execution in the content process by exploiting a use-after-free in Animation timelines. We have had reports of this vulnerability being exploited in the wild."

See:

- NVD page for CVE-2024-9680: https://nvd.nist.gov/vuln/detail/CVE-2024-9680

- Mozilla security advisory: https://www.mozilla.org/en-US/security/advisories/mfsa2024-5...

New comment by statusfailed in "Were RNNs All We Needed?"

statusfailed — Thu, 03 Oct 2024 18:01:00 +0000

I only had a quick look, but it looks like they tweaked the state update so the model can be run with parallel scan instead of having to do it sequentially.

ConsiStory: Training-Free Consistent Text-to-Image Generation

statusfailed — Mon, 09 Sep 2024 15:03:51 +0000

Article URL: https://research.nvidia.com/labs/par/consistory/

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

Points: 2

# Comments: 0

New comment by statusfailed in "Why AI Infrastructure Startups Are Insanely Hard to Build"

statusfailed — Wed, 03 Jul 2024 08:36:02 +0000

I'd love to know what your use case is that makes those things important to you - and what kind of benchmarks and cleaning tasks do you need to run?

Also, what kind of evaluations for quality of reasoning do you use?

New comment by statusfailed in "Sending emails to my three-year-old"

statusfailed — Mon, 10 Jun 2024 17:44:30 +0000

This lets other family members send emails too, and has an interface everyone is familiar with.

New comment by statusfailed in "Launch HN: Univerbal (YC W23) – Language learning with a conversational AI tutor"

statusfailed — Tue, 30 Jan 2024 19:22:35 +0000

At least for chinese there are off-the-shelf word segmenters you can use like jieba[0]- I used it in gptlingo and it Just Works(TM).

The "show pronounciations" setting just turns on pinyin above characters - what I want is to type pinyin and enter chinese characters. Actually showing the pinyin above characters is quite distracting!

[0]: https://pypi.org/project/jieba/