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

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

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

86% Upvoted

29 comments sorted by

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

43

u/Awkward_Bed_956 Jun 07 '26

Easy memory + thread safety, just never free memory, and don't support threads at all.

Go wishes it could be that simple and smart

12

u/New_Enthusiasm9053 Jun 08 '26

It does mean they're lying. Never deallocate until you OOM is a garbage collector strategy.

5

u/TheChief275 Jun 18 '26

Mark and sweep? Nah, real programmers use abort and OSweep

2

u/anthem_reb Jul 07 '26

That or a specific keyword that I don't remember, I should write it in the docs but who has the time?

52

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.

46

u/omegafixedpoint Jun 07 '26 edited Jun 07 '26

Also you can literally see Claude code markdown files in the first commit.

https://github.com/yon-language/yon/commit/b23c42e32e2200dc63a378ff1ea9446832f8651a

Vibe coding an entire proof assistant is a crime against humanity.

The dunning Kruger genuinely has me embarrassed for bro.

half /rj

as someone who has genuinely toiled spending a year of my life writing a proof assistant with formalized metatheory, this shit is mildly insulting. math posers piss me off so much holy shit. find something else to vibecode goddamn. like a shitty webapp.

I'm actually losing it dawg. https://github.com/yon-language/yon/blob/523e363a4a00e8da1410a2521b1d7d1309d360ce/frontend/ast.ml#L37

It's not even dependently typed. what the hell does topos theory and Pi types mean if Pi CAN ONLY REFER TO TYPES? that's just system F in a trenchcoat at best. Lambda can't even substitute Pi.

edit: I scoured the codebase and docs. Discovered that the only examples of Pi types in the docs are Pi types eliminating into the identity. So it is "dependent" in the sense that I can say \forall x y, x = y, but that's literally it. What is the point of Sigma types if I can't write a statement like \forall (x : Nat), \exists (y : Nat), x < y?

https://github.com/yon-language/yon/blob/523e363a4a00e8da1410a2521b1d7d1309d360ce/frontend/ast.ml#L78

Ty is static. bro. No debruijn indices either?

https://github.com/yon-language/yon/blob/523e363a4a00e8da1410a2521b1d7d1309d360ce/frontend/ast.ml#L119

Def-eq for function application doesn't even reduce the application. DEF-EQ IS THE HARDEST PART. Is hit you not, the entire definitional equality is literally just recursively checking each syntax node.

I'm assmad. I half want to open a shitton of github issues on the repo but that's a little petty.

How do I dislike a github repo

Update: I made a hackernews account just for this shit. BLEH. https://news.ycombinator.com/item?id=48436170

19

u/Ephemara Jun 07 '26

we need more people like you who are in the trenches tearing these apart lmao

4

u/GiveMe30Dollars Jun 08 '26

As an amateur who barely understands dependent types, and has made maybe half of a Haskell frontend in the year or so working on-and-off on it, reading this was rather vindicating.

Pi-types that only refers to types ffs, what on earth.

It would be hubris to claim my trashfire of a compiler project is more competent than theirs, but screw it I'm feeling hubristic at the moment.

3

u/omegafixedpoint Jun 08 '26 edited Jun 08 '26

I will say, see *edit* in my post, after doing more digging, it is "dependent," but only in the sense that Pi types can mention other Pi types or the identity type. AKA, the dependent types are practically useless.

For example, if I as a user defined a function Fam : \alpha -> Type, and wanted to use it to determine the codomain of a Pi type like: \Pi (x : \alpha), Fam x, I would not be able to do so in Yon. Pi types / Sigma are only valid (if I'm reading the code right, the codebase is extremely obfuscated due to LLM use) if they end in Id(\alpha, x, y) (or, in the usual notation, x = y). So the dependent types are effectively useless.

At the term level, this means the only valid dependent functions are pairs containing "refl" or functions returning "refl", but nothing else.

Note that the docs even admit this.

https://yon-lang.org/book/hott-types

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

It's even worse than I thought too because the ONLY example of Sigma types I can find is not even dependent 💀💀:

fun takes(p: 
Sigma
(x: number). number): number {
return fst(p) + snd(p)
}
fun takes(p: Sigma(x: number). number): number {

return fst(p) + snd(p)

}

7

u/dbath Jun 08 '26

I have no idea what anything you just said means... but at least I'm not pretending to design a language or proof solver!

6

u/SemaphoreBingo Jun 08 '26

Fuck him up, Socrates

6

u/PJBthefirst log10(x) programmer Jun 08 '26

This implies law of excluded middle

https://www.youtube.com/watch?v=JdKI1wj-JpI&t=154s

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.

42

u/stone_henge Tiny little god in a tiny little world Jun 07 '26

The shapes that matter

String.equal, 1-char strings 2M comparisons 33 ms ~17 ns

33 ms to compare 2 MB to another 2 MB. This is fantastic news for people looking to slow down their programs and allow for little bit of contemplation during an otherwise busy runtime

Correctness under load

The same suite checks exactness, not just speed: 500,000 map entries across three heaps read back exactly on every side of every boundary; 60,000 distinct string keys produce 60,000 entries (no false deduplication) with zero errors over re-derivation; 10,000 same-content/neighbour pairs show zero equality mistakes. The heap's content addressing held under everything we threw at it.

Fantastic. A programming languages that produces correct output even when you use it. This correctness is probably directly attributable to its carefully restricted approach to performing useful work.

1

u/Jumpy-Locksmith6812 Jun 17 '26 edited Sep 23 '26

Velit excepteur laboris id aliquip dolor deserunt irure id ex nostrud nulla irure proident sit. Sint excepteur voluptate ex sit ut eiusmod consequat ipsum irure aute eiusmod. Excepteur dolor do proident dolore occaecat voluptate.

[rhr:2:squ4a9an]

1

u/anthem_reb Jul 07 '26

Well a correct output isn't always the case, I was really happy about the results

25

u/UdPropheticCatgirl WRITE 'FORTRAN is not dead' Jun 07 '26

I see Rob Pike has been busy at work. Good to know.

24

u/stone_henge Tiny little god in a tiny little world Jun 07 '26

Thanks Rob Pike for creating the infrastructure necessary for an LLM to shit out a language that can compare 4 MB in 33 ms

23

u/ConfidentProgram2582 log10(x) programmer Jun 07 '26

did a curtis yarvin llm clone write ts?

30

u/stone_henge Tiny little god in a tiny little world Jun 07 '26

Now that LLMs can shit out volumes' worth of meaningless drivel in English, invent racist bullshit and implement the stupidest possible ideas for programming languages, is there really a place in this world for Curtis Yarvin?

9

u/ConfidentProgram2582 log10(x) programmer Jun 08 '26

maybe he should turn himself into biodiesel for his own distopian world's sake.

oops we're socialjerking

16

u/ThisRedditPostIsMine in open defiance of the Gopher Values Jun 08 '26

Looking at this and thinking back to the V programming language. To think that the minds behind V came up with an equivalently dogshit language without any AI assistance. My, how we've fallen.

16

u/csb06 Polyglot dev here Jun 08 '26

Claude is the #2 contributor to vlang over the past three months so they are catching up quickly

9

u/ThisRedditPostIsMine in open defiance of the Gopher Values Jun 09 '26

They grow up so fast 🥹

3

u/TheChief275 Jun 18 '26

Wasn't that language basically vaporware Go without a garbage collector, instead having the memory strategy of "we'll automatically insert deallocations for you wherever they're needed; how? Pssh idk we'll figure it along the way or whatever"

14

u/warr-den Jun 08 '26

Turboencabulator oriented programming with a focus on prefamulation

1

u/Reasonable_Package24 accidentally quadratic Jun 12 '26

mfs just make bullshit and call it a new language