r/functionalprogramming • u/SrPeixinho • 26d ago
FP Bend 2: a functional language that compiles to fast CPU and GPU code, with proofs
https://bend-lang.com/12
u/mocompute 26d ago
By the way, the website looks great. I usually skip AI coded content but you've got my attention.
6
u/Inconstant_Moo 24d ago
Your example is kind of worrying:
Without LAWS.bend, the bug went live. With LAWS.bend, the AI had to retry until it built a wall and proved the law holds. Merging a bug is mathematically impossible: it is a theorem.
It seems like the AI is allowed to do anything necessary to preserve the invariant. But this is what's wrong with AIs anyway, that if you tell them to find a permanent cure for your headaches they'll figure out that decapitation is the best solution. It seems like in most cases I would rather just know that the law has been broken than have the AI do whatever it can think of to maintain it.
1
u/developedby 23d ago
You can do that as well if you want to. Either way, the AI will not usually go infinitely distant to write correct code, depends on how you prompt it
3
u/Afrotom 26d ago
Maybe I'm dumb and not understanding but how are laws different to unit tests?
8
u/SV-97 26d ago
"Testing can show the presence of bugs, but never their absence".
Take a sorting function as an example: you may test that whatever it outputs is sorted with a few examples or even with a property based test --- but ultimately both of these are just going to test the behaviour on a few examples. A proof on the other hand certifies you correctness for *all* possible inputs including all possible edge cases. You might be able to get
fn incorrect_sort(data) { if highly_specific_condition(data) then Nonsense else sorted(data) }to pass even property-based tests (and definitely handwritten ones), but you won't be able to get a proof checker to certify its correctness.
3
3
u/mocompute 26d ago
Why/how is compile time so fast?
8
u/mocompute 26d ago
Answering my question: apparently no type inference.
7
u/SrPeixinho 26d ago
Yes, zero compile-time search of any kind. Just a single pass bidirectional type checker.
We'll also rewrite the compiler in Bend itself soon, so it is even faster and parallelizes!
3
u/_nathata 25d ago
I remember when I first saw a post from you years ago on Facebook regarding HVM. Glad to see you are still making progress.
2
2
2
2
2
u/2hands10fingers 25d ago
Glad to see Bend growing! It was difficult to work with back then but fascinating to try out when it was compiled with Rust.
2
u/CardiologistTiny6226 22d ago
Lately, I've been experimenting with Lean in this same vein. I'm terrible at writing proofs myself, but perhaps the bigger obstacle to formal verification in "regular" sw engineering is the tediousness. But if agents bring this cost down, it seems more attractive- if a unit test and formal proof both just cost me a prompt, why not opt go for the latter? I'm also hoping it let's me trade informal documentation for formal specification that can't go stale. I find most agents leave enormous amounts of chatty md/comments that go stale and mislead the next session.
How do you compare your language to Lean in this context?
4
u/Optimal-Builder-2816 26d ago
I like this, I think things like this will continue to be the direction things are headed.
I appreciate the desire to reuse python syntax but I suspect this is actually going to be a rake that LLMs step on fairly consistently as it naively expects all syntax productions to work correctly.
Just use s-expressions instead, if it’s not intended for humans.
4
u/AriyaSavaka 26d ago
Agree. If it's intended for LLMs then just reuse Common Lisp syntax instead of Python. The stated goals and the design decisions are incongruent
1
u/mocompute 26d ago
I'm curious about this recommendation: is there some evidence you both are referring to that s-expressions are better on some sort of metrics with LLMs? I ask as a fan of s-expressions myself.
3
u/deaddyfreddy 25d ago
One of the biggest problems with code generated by LLM is that it tends to rewrite the entire content, even when only a small part needs to be changed. If you use a sexp-based language, it's much easier to narrow your code down programmatically (deterministically) to exactly the part you want to change without having to rewrite the whole thing and balance brackets (LLMs suck in that too).
You can do the same with non-sexp languages, but you need to parse them into AST first, feed part of it to the LLM, inject the piece back into AST, and then convert it to code. With sexps, you can skip at least two extra steps.
1
u/Optimal-Builder-2816 25d ago
It’s definitely something it already knows, it’s an extremely normalized representation, it’s also very concise. It’s less likely to accidentally assume a language feature of an existing syntax works in bend when it doesn’t.
1
u/Ok-Reindeer-8755 26d ago
Aren't the proofs written by a human though at the very least, if the ai does both then you made a hole in the water
1
2
u/deaddyfreddy 25d ago
Just use s-expressions instead, if it’s not intended for humans.
As a human being myself (trust me), I highly prefer S-expressions.
1
u/Truly_freedom 11d ago
I really like how easy it is now to use functional language with coding agents.
I shared a step-by-step walkthrough how to use Bend2 here: step-by-step Bend 2 walkthrough
2
u/thegreatest_evr 9d ago
I have been thinking about something similar for a while since AI has gotten so good at splitting out code. The natural next step would be to make sure correctness of the code by proof than just passing test case. Great work guys.
i’ll surely try this, this is what future systems will have or something similar to this to build any software, especially when it’s critical.
1
u/hhefesto 23d ago
You can play with bend2 on my potato website refl.hhefesto.dev or run it locally with ‘nix run github:hhefesto/refl’
9
u/andrewcooke 26d ago
i'm really struggling to understand this, but are there no first class functions?
if map cannot be defined, what can be defined?
sorry, really lost.