statusfailed

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

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

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?

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

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

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!

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

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 [email protected]

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?

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

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 [email protected]

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

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.

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?

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

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/

> Duolingo is good at going from nothing to something

Seconding this. I got noticeably better at Chinese after using duolingo every day. I feel like I hit a ceiling now and it's not helping too much, but it definitely worked.

OK I played with this some more, it's so good - exactly what I dreamed of!!

A couple more bits of feedback:

(1) The "suggestion" / "I'm unsure" etc. feedback is fantastic

(2) Word segmentation doesn't seem to be working properly, and so the context lookup doesn't work right. Example:

中国 should be parsed as a single word ("china"), but it's parsed as individual characters ("middle", "kingdom").

This means I have to tab out to a dictionary to look up words, and it's a bit annoying to select the right text.

Nice! I built the same thing to learn chinese[0], it even has the in-context word lookup!

I have a feature request: if I don't have a pinyin IME installed, it's very hard to use - it would be nice to have an in-browser one!

[0]: https://github.com/statusfailed/gptlingo

I used postgrest (without htmx) on an old project; it's impressive how far you can push it. HTMX seems like a perfect fit for it too, although I'm not sure how much I really want to maintain htmx templates inside SQL functions...

Location: London, UK (able to work in the US without visa) Remote: Preferred Willing to relocate: No Technologies: Python, Haskell, Rust, HTML/CSS, Javascript, AWS, Terraform, Postgres, & more. Résumé/CV: https://statusfailed.com/files/cv.pdf Email: [email protected] Website: https://statusfailed.com GitHub: https://github.com/statusfailed

I'm a technical generalist with 10 years experience and a Ph.D in CS focusing on category theory and machine learning. I've worked in a variety of roles both full-time and contract: Full stack developer, data scientist, pentester, and machine learning researcher. Most recently I was awarded a grant to develop a differentiable IR for zero-knowledge machine learning[0].

[0]: https://yarrow.id

I'm in the same boat- I just want a simple headset that overlays a big, high-resolution monitor on my normal vision. The closest thing I know of is the [Simula One](https://www.simulavr.com/), which seems to be a VR "virtual monitor".

VR instead of AR is a dealbreaker for me though- I want AR virtual monitors that overlay the displays on my actual vision. Even VR which uses a camera to pass through to the display isn't really what I want.

My ideal hardware would just be a "dumb" AR display with wide FOV and an HDMI input that just overlays the video data onto my normal vision.

From what I understand a big challenge is the wide FOV though, but I don't know enough about optics to really understand why this is the case.

What kind of applications do you see for training on mobile devices? Is anyone using this in industry?

I (as a Ph.D student) paid open access fees with my own money. Not grant money, my own salary.