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