upvote
Again, very strange

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

reply
That's a start-up style marketing: when you make a product you focus on a big vision and positive sides and de-emphasize weaknesses. I'm afraid that's actually 100% Victor's decision to do it this way, and it seems to be working in terms of generating hype: it got ~4k likes on X, which is a lot for a new language.

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

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

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.

reply
A complete implementation have been released, how is that not a substantiation?

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

reply
How do you know the implementation is complete or that it works well?

Have you evaluated it?

Wouldn’t you be inclined to withhold any claims of anything being substantiated until it’s actually been evaluated?

reply
Wait what? Have you? Why are you posting passive aggressive unfounded dismissals posing as questions?
reply