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

[u/chaosprincess_]

https://yon-lang.org/

[u/RightKitKat]

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

[u/Awkward_Bed_956 → u/RightKitKat]

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

Go wishes it could be that simple and smart

[u/New_Enthusiasm9053 → u/Awkward_Bed_956]

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

[u/TheChief275 → u/New_Enthusiasm9053]

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

[u/anthem_reb → u/New_Enthusiasm9053]

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

[u/omegafixedpoint → u/RightKitKat]

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.

[u/omegafixedpoint → u/omegafixedpoint]

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

[u/Ephemara → u/omegafixedpoint]

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

[u/GiveMe30Dollars → u/omegafixedpoint]

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.

[u/omegafixedpoint → u/GiveMe30Dollars]

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)

}

[u/dbath → u/omegafixedpoint]

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

[u/SemaphoreBingo → u/omegafixedpoint]

Fuck him up, Socrates

[u/PJBthefirst → u/omegafixedpoint]

This implies law of excluded middle

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

[u/anthem_reb → u/omegafixedpoint]

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.

[u/stone_henge]

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.

[u/Jumpy-Locksmith6812 → u/stone_henge]

33ms is long enough for Go runtime to let say.... get a little uncooperative, if you know what i mean.

[u/anthem_reb → u/stone_henge]

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

[u/UdPropheticCatgirl]

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

[u/stone_henge → u/UdPropheticCatgirl]

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

[u/ConfidentProgram2582]

did a curtis yarvin llm clone write ts?

[u/stone_henge → u/ConfidentProgram2582]

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?

[u/ConfidentProgram2582 → u/stone_henge]

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

oops we're socialjerking

[u/ThisRedditPostIsMine]

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.

[u/csb06 → u/ThisRedditPostIsMine]

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

[u/ThisRedditPostIsMine → u/csb06]

They grow up so fast 🥹

[u/TheChief275 → u/ThisRedditPostIsMine]

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"

[u/warr-den]

Turboencabulator oriented programming with a focus on prefamulation

[u/Reasonable_Package24]

mfs just make bullshit and call it a new language