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

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

Sorry. See the edit at the top if you haven't already. I didn't realise how much it came off as a critique of you rather than a particular approach to software engineering.

It's easy to write something and have a model of what you're writing in your head that is massively different from how someone else will read it without realising, not that that excuses it.

---

I disagree with LLMs manually writing proofs without other tools doing all the work they possibly can ever being a good solution for a couple of reasons:

1. Tokens are really expensive when we have a LLM spending hours hacking aware at a proof, not to mention generating those tokens is slow.

2. The context window becomes flooded with proof work rather than work on the original problem, which will lead to a worse solution. LLMs are demonstrably worse at writing code when you continue a session on a new task instead of starting a new one.

> It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly.

We can cache the results and help the checker along with assertions rather than throwing out all the smart parts of the checker.

I was really confused when reading the article that their claim is you don't know formal verification, I was expecting something way juicer.

Hi! I'd like to know how bend2 differs from Hoare logic or Lean?

Hi!

I'm just leaving you a comment to counter the influx of negativity coming towards you for no reason.

I hope you are doing well and won't take all this too badly -- try to think of it as just free marketing for your project!

Have a nice day!

I was with you until this.

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

Are you being facetious? Because I've seen some bad takes from people trying to justify their AI coding practices, but this is the first one that actually made me laugh. It's clear that this public attack has you in a defensive mental state (which is perfectly understandable), so giving you the benefit of the doubt, I won't pile on and take everything you're posting too seriously.

However, I gotta point out how ridiculous this statement is, because it's the kind of thing that'd make me wonder if someone has any programming experience at all. Typing speed is not, never has been, and never will be a limiting factor in software development. "I didn't do <X> because of <reason> even though I totally could" is a pathetic cope.

It kinda reminds me of a recent post from John Carmack where he said (paraphrasing) that he originally wanted to release Idtech to the public domain as a "gift to the world", but couldn't do it because of his pesky business partners, but he totally would've done it. Let's just ignore the part of the story where he became filthy rich from licensing his software, and focus on how good it will feel to call it a "gift to the world" when an AI company integrates your code into their commercial products without licensing it from you.

>That is what makes Bend realistically 10x-100x faster than every alternative.

Do you have benchmarks which show this?

[dead]