Top
Best
New

Posted by nicolas-siplis 13 hours ago

Bend – A language that blocks AI mistakes via proof, on CPU and GPU(bend-lang.com)
446 points | 209 commentspage 2
jmakov 3 hours ago|
Is there an overview on how this works? E.g. if we code a contract in LAWS.bend, how is it enforced? What prevents my LLM model to skip a contract?
hollowturtle 12 hours ago||
Would the author have specified on the page that it's a fast new language with a new take on proof and so on, without mentioning ai and that alone would have caught my attention. It seems like if there isn't the word ai people are not interested anymore, we used to care many of us used to care
txhwind 3 hours ago||
I'm interested in how to integrate formal verification with existing software libraries. For example, https://github.com/verus-lang/verus integrates proof with macro in Rust. What's the plan for Bend?
chaidhat 11 hours ago||
I think this is premise for AI: Lean and formal verification seems more and more important in today's world and I think a variation of programming language like this is bound to win. This, or a library or framework to prove typescript.
LightMachine 9 hours ago|
should I read this as "I wish I could find a guy like you" :')
fzaninotto 3 hours ago||
Trending idea! On the same subject, but aimed at compatibility with TypeScript, I just discovered Code Contracts.

https://code-contracts.cc/

fudged71 12 hours ago||
Congrats on the launch!

Question, does the parallelism work on M-Series GPU? The page says CUDA parallelism but shows Mac performance numbers.

LightMachine 10 hours ago|
Thank you!!

Currently, parallelism works in any multi-core CPU, and in Apple M-series and NVIDIA GPUs.

hmokiguess 11 hours ago||
So sad that commit history is a thing we can feel emotionally attached to a point of feeling vulnerable when releasing it with others.

Also equally sad that without a way to relate easily with how something came to be (e.g. the commit history) others will struggle focusing at the work and will judge its lineage.

I guess to folks here confused by that go search SrPeixinho on Reddit and that should have a lot of history for you to understand the background of the work, and you can also join their Discord server and literally talk to them there.

LightMachine 10 hours ago|
I'll try to sanitize the commit history, I had no idea it would be so important
LightMachine 7 hours ago||
Commit history is back!
NortySpock 5 hours ago||
"You only have 10 seconds to make a first impression"

Glad you were able to restore the commit history.

With all the lack of authority of a random software developer on the Internet (but feel free to check my post history), I see the GitHub repo and its commit history as important and answers a few questions.

How old is this project ? (If one commit, I have no time range, so I have no way to know how long it has been worked on .)

Is it regularly updated? (If one commit, I can't tell the pace of updates)

Is it just one person, or a few people, or a community? (If only one commit, cannot see how many other people are available to support the project.)

If a project has no issues (no user complaints), then it's probably not used by anyone -- throw a rock and you can get one person to complain about how you changed the scenery, one person to complain about it being loud, one person to complain about how you threw it unergonomicly, and one person to criticize your accuracy. :) If it has no issues then probably no users.

Does it have any merged PRs? Open PRs? (If no merged PRs then presumably you do not really accept them? No way to know for sure but it's a signal.)

Of course these metrics can be gamed. But if you literally have only one commit, no issues, no PRs, then it's like declaring your restaurant is open for business but all the lights are off, there are no patrons, waiters, cooks, and there is a single to-go box on the table with a small bell next to it. Or it's a museum with only one exhibit and no docents or guests. It's just incredibly odd to see no history for a project.

LightMachine 5 hours ago||
yeah that makes sense, thanks for the feedbacks!
pron 11 hours ago||
> In the post-AGI economy, humans will eventually stop writing and reading code, but we still need an ambiguity-free way to tell the AIs building the world around us what we want done.

Why? Won't an AI that can correctly write any program (and make any change) also be smart enough to know what exactly we want better than we can explain, at least ahead-of-time?

If AGI means "human level", why is there any part of the process that humans will be needed for, especially some engineering aspect?

> With proofs, we can verify that the AI implemented our prompts correctly.

Certainly such an AI would be able to just write machine code directly and verify it through whatever means, including formal proofs, as needed. Why does it need a compiler?

I think that an AI that's smart enough to write almost any program and prove almost any property, will also be smart enough to not need to communicate with us formally and rather answer every question we have (and proofs are not always necessary, as they're not always necessary today), and probably also smart enough to figure out what we want built. It's probably capable enough to replace the software's users, too. I don't understand why it's likely that we'll have AI that's so capable to write all software correctly, yet not capable enough to do things that are probably easier.

lacedeconstruct 11 hours ago||
An AI smart enough should act like a senior engineer gathering requirements, it should start with assumptions and poke at different areas with questions until it has a complete idea, when I talk with a client I dont expect him/her to really formalize all the details its my role to question them until all the sharp corners are covered
pron 11 hours ago||
Yes, but also, who do you gather requirements from? Other people. But if we're talking AGI, then these other people, i.e. users - or at least those who define the requirements - could be replaced, too.
ModernMech 8 hours ago||
> Certainly such an AI would be able to just write machine code directly and verify it through whatever means, including formal proofs, as needed. Why does it need a compiler?

If the AI can write the program bytecode through AI magic, why can’t it verify that it works through AI magic?

The AI needs a compiler for the program for same reason it needs a proof language to verify it.

pron 59 minutes ago||
We used to write programs without a compiler. We'd write them in Assembly. The AI won't even need the assembler. If verification is done through formal proofs, a logic language is, indeed, needed, but the program itself could remain in machine code.
ifiht 5 hours ago||
Well, didn't win, but definitely broke it. Needs an edge case handler for tool call exhaustion:

This prompt has used its 30 tool calls. Send another prompt to go on. Error: This prompt has used its 30 tool calls. Send another prompt to go on. continue. No tool output found for function call call_2CRNfB1hmI1v74YCDDcvP1EN. Error: No tool output found for function call call_2CRNfB1hmI1v74YCDDcvP1EN.

lucaslazarus 8 hours ago|
This seems less like a proof and more like a "pretty please" with test cases?
More comments...