Yes, it doesn't look like a paper at all. I can see the idea, and it's an interesting idea, but no proofs that it works, no measurements, and no proper citations.
Nobody claims Victor hasn't done a lot of research. But academically inclined people typically expect claims to be substantiated either formally or empirically or both.
Academic people might have more trust in a paper which when through a lengthy publication process. But if you think about it, it's not a better proof than a direct access to the thing. It used to be hard to try out software but with modern tech it literally takes minutes...
Have you evaluated it?
Wouldn’t you be inclined to withhold any claims of anything being substantiated until it’s actually been evaluated?
The person I am responding to made a SPECIFIC claim when they said, “A complete implementation have been released”
They then ASKED, “how is that not a substantiation?”
Uploading code does NOT substantiate anything.
The code must been executed, tested, analyzed and/or verified in order to substantiate ANYTHING.
We are in limbo because MOST people are JUST seeing the code now. Almost nobody has evaluated it.
BTW, I got the Discord announcement BEFORE I saw the HN announcement (Because I’m not a hater or a bully) and I started looking at the Lean code as well as the TypeScript compiler.
Have YOU been evaluating it? Do you actually have an informed opinion, or are you here to fight the bullies?
Are you arguing with me or the parent who actually called it “sus af”?
External parties can’t do any meaningful discrimination between human and agent effort when the agent is doing the communicating. One may only read what’s there
I’m not saying that the author is inept or that they have done no work. There can be plenty of great underlying mathematics behind something that is vibecoded.
The reason I worry about the use of agents here is not because it invalidates any ideas or research done by the author; rather, it editorializes and oversells. It presents the claims of the work as an all encompassing solution to all of the worlds problems
There may very well be tons of great ideas here. However as presented, it reads as though the language is the solution to creating vibecoded apps and is equipowerful to state of the art proof assistants while being orders of magnitude more performant. That is a huge claim that has not yet been substantiated, and I do not believe that solely a human is currently making that claim
Regarding substantiation -- they released source code and demos. As far as I understand, the weakness is that proofs are very verbose as there are no strategies. etc. However, they are making a separate service for making these proofs using proprietary technology: https://bend-lang.com/bender
Calling this "a random vibecoded project" is rather disrespectful, don't you think?
Regarding the paper, he states it clearly "designed by the human author". That's not at all the same as just asking Fable to write a paper. I mean the important thing is ideas, not the way they are described.
Please tell me how "I'm glad you're having fun vibecoding" is not disrespectful?
I thought that you thought Bend web site is all that is to it and wanted to point to relevant information. But if you think that "having fun vibecoding" is an appropriate thing to say to somebody who spent many years doing research, I don't know what else to say.
Again, as a "proof of research" take a look at : https://github.com/VictorTaelin/Interaction-Type-Theory that's 3 year old, pre-dates Fable, but OMG doesn't look like a paper.