LightMachine

I don't think that means it was "unsuccessful" in the sense you imply, though, because the project was never meant to be used in production. It was there to display a milestone (running inets on the GPU) and I was very clear it wasn't ready to be used yet. For example, it had only 24-bit integers, a 2 GB memory cap, and other limitations that made it unpractical. I still don't know why it has so many stars. I posted it to hacker news and that just happened. I guess it just went viral without really being ready yet, which got us to where we are now.

Anyway the commit history is back now. I apologize for nuking it

Comment · 1 month ago

It will, there is just too much to do! It is a programming language. With a consistent, non-standard proof system. That compiles to GPUs. We're a small team. Please be patient

Comment · 1 month ago

Victor here. I haven't "worked" on Formality. I've founded it. Designed every part of it. Before LLMs!

sighs

Here's my response to this ridiculous accusation: https://news.ycombinator.com/item?id=49753898

I can't internet anymore. I need a beach

Comment · 1 month ago

Note that using linked lists for strings is actually more "parallel friendly" because you can take the head/tail and spread it around 16k GPU cores in O(1), unlike in Haskell, unlike arrays, which require a linear copy, becoming quadratic. So, the right "default type" isn't that clear on Bend, because GPUs behave very differently from CPUs.

That said, yes, we definitely should have a compact Text type. I'll add it over the weekend.

Comment · 1 month ago

1. LLM inference is cheap compared to the cost of a bug, and you can use tools to automate the proof-work, as you said so yourself.

2. Why would it? The AI shouldn't load already completed proofs, only their type signatures (which are one liners). Sounds like you're projecting bad context management?

Caching only works until you change a deeply nested constant. Then you must wait 2 hours as Lean re-checks every transitive dependency of a massive simp-ridden codebase. Also, first time check time IS relevant to UI. Nobody wants to wait 2h to start using a library after they first download it. Perhaps you don't mind that but I do; that's the kind of bad UX that made me go for that design choice on Bend. Which again, may be wrong or may be right. But it was intentional.

Having a checker that is just fast by construction, regardless of caching, was a top design priority, and I weighted it over verbosity in a layer I believe nobody will be reading anyway.

Comment · 1 month ago

The history is back...

Comment · 1 month ago

(Author here) What about it isn't working for you?

Also, wrote a response to this whole thread here:

https://news.ycombinator.com/item?id=49753898

Comment · 1 month ago

So are Haskell's, since 20 years ago, with no options for years?

We will introducing binary buffers eventually. The project is new...

Comment · 1 month ago

"The developer has built an entire language around a field seemingly without realising that said field exists."

That is incredibly funny.

Here's a talk about formal verification I made 7 years ago @ DevCon:

https://www.youtube.com/watch?v=0fg1QbeeqNU

Here's Cedille Core, my implementation of Aaron Stump's self types, a Computer Science professor who taught me a lot, ~8 years ago:

https://github.com/VictorTaelin/Cedille-Core

I also implemented Kind-Lang 5 years ago, way before LLMs:

https://github.com/higherorderco/kind

I dropped out of Federal University of Rio de Janeiro to study this subject independently, because I was passionate about it, and I spent nearly 10 years doing so, daily, on weekends. That's what I do.

Bend proofs being verbose has nothing to do with me not knowing that inference, unification, or program search exists. Kind had these, 5 years ago. In fact, I've also been researching the later, and I built SupGen, which overperforms every published symbolic program synthesizer in the literature by 10x or so. This is unpublished yet, but you can find my posts about it 2 years ago on X (I'm @VictorTaelin).

So, why is Bend verbose???

Because it makes it fast. It is intentional. It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly. That is what makes Bend realistically 10x-100x faster than every alternative.

But wouldn't that mean it is much harder to write it?

No. As you said it yourself, we have tools that can fill these proofs today! Not just AI models. You can apply these tools to produce Bend proofs, while the language itself remains a thin, dumb proof kernel that does one thing, and does it well.

If nobody is reading these proofs (because they're written by AI and automated tools), then, it is, in my opinion, irrelevant, as proofs will eventually become a layer nobody looks at, just like generated assembly.

Of course, I could be wrong here!

But it is misleading, if not just a bit malicious, to claim I "vibe-coded" a language without knowing about a field I've spent a decade researching about.

Every single part of Bend is an intentional choice I made after considering every alternative. I use LLMs to fill code after I make all hard architectural decisions because they type faster than me, and I'd rather spend my time doing useful experiments than typing trivial functions, even though I could.

Incidentally, deciding what I should NOT include took me way more time and effort than any line that was shipped, and there are perhaps millions of lines of code, manually written by me, that I threw away, backing up these 4k that went into the final design. An artist once told me you must first paint a Rembrandt before you can draw a cartoon that's simple in the right way, yet that might mislead someone who has never drawn into thinking you don't know what you're doing. I guess.

Comment · 1 month ago

yeah that makes sense, thanks for the feedbacks!