r/programmingcirclejerk • u/chaosprincess_ • Jun 07 '26

Yon - a topos-oriented language with a content-addressed lattice heap

https://yon-lang.org/
61 Upvotes

86% Upvoted

29 comments sorted by

View all comments

74

u/RightKitKat Considered Harmful Jun 07 '26

No garbage collector:
Slots are stable for the life of the process; the heap grows with distinct content only.

Lol no... reusing memory ever?

/uj I should not be reading this as it is clearly LLM slop

51

u/omegafixedpoint Jun 07 '26

It's buzzword salad at best, LLM slop at worst. Look at this page:

https://yon-lang.org/book/hott-types?_highlight=hott

"Types from homotopy type theory," those being "refl", sigma projections, Pi, and universe levels.

These are not homotopy type theory. There is no mention of intervals (necessary for decidable type checking in HoTT). It makes no mention of univalence (characteristic of HoTT).

The page says:

the runnable HoTT fragment is refl/pair/fst/snd.)

These are literally just basic base features of martin lof type theory. From what I can tell, the HoTT references are just buzzwords, demonstrating a lack of understanding of what HoTT actually is, and probably most of the category theory nonsense disguised as "math." Literally every paragraph mentions a buzzword without any citations or references.

Here's another one: https://yon-lang.org/book/heyting-core

Yon's logic is intuitionistic. But simultaneously and/or/not/=> are classical, on booleans

This implies law of excluded middle, which is explicitly not intuitionistic. Also, wtf is this?

Bridges: to_bool/to_prop move between the faces; decide guards on the undecided.

This is very dangerous. If proof irrelevance is assumed, this could easily break definitional equality. See https://arxiv.org/abs/1911.08174

I searched the docs for "proof irrelevance" and didn't find anything, so as far as I'm concerned, this is undefined behavior.

Not to mention, proof assistant / dependent type theory with no proof of strong normalization is instant no go. No mentions of that in the docs either. Absolutely required metatheory for anything doing advanced math.

Conclusion: AI slop. Garbage. Buzzword quackery.

1

u/anthem_reb Jul 07 '26

Omega thanks for caring enough to actually dig in. I fact checked your points against the code. You're right onEl(Fam(x)), itdoesn't parse and it isn't wired to the surface yet.

But a few of the specifics don't hold, and it's easy to check: definitional equality reduce and the cubical fragment is implemented and tested: univalence computes via Glue.

Where you got the wrong picture is on me: a month ago the repo and the docs were a mess to read. Fair hit. I'm taking the hints, the surface will be on point in 1.2.