Tests aren't proofs.

> All these skeptics and nobody just tried it out?

Welcome to HN!

May I remind you of the Dropbox comment? https://news.ycombinator.com/item?id=9224

I gave it a spin using muse 1.3

Got it to port kaparthys microgpt -> https://github.com/thomasdavis/bend-experiments/tree/main/mi...

muse did surprisingly well getting it to work, can't speak for the code quality.

The benchmarks: https://github.com/bendlang/bend/tree/main/bench

The script we use to run them on our servers: https://github.com/bendlang/bend/blob/main/gates/perf.ts

Read the damn code and readme, for god's sake!

nigga doesnt know about solarized light

It's just solarized, i imagine most developers are familiar with it

He got 80k+ followers on Twitter (x), tracking his progress on Bend, why sus?

Is EC2 real-world enough? From June:

https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng...

And for the PQ parts of Apple's crypto libraries, from May:

https://security.apple.com/blog/formal-verification-corecryp...

Similar from Microsoft, from July:

https://www.microsoft.com/en-us/research/blog/verifying-rust...

Funny you say that while OpenAI and rest of the world rely on Lean and other formal systems to power through (or sometime brute force) math problems.

I’m just looking at it for the first time myself, but isn’t the compiler in https://github.com/bendlang/bend/blob/main/bend2/comp.ts ?

the compiler is in comp.ts, alongside the runtime

it is not a pretty file and it has a lot of gambiarra and AI slop for now

if you want to read something worthy, read the kernel (bend.ts)

And benchmarking this language against Isabelle/Agda/Lean/Rocq is strange. The time taken for those systems to perform their checks is mostly spent on elaboration, which includes unification against metavariables, typeclass resolution and tactics. Bend has none of that (there are no type classes or traits, and according to the README, everything must be fully annotated and nothing inferred). This means that the benchmark is comparing Bend's checker to the other systems' elaborators + kernels rather than their kernels (Agda doesn't have this separation though). The latter would be a fairer comparison, and in this area the other systems are already fast. Framing it as "outperforming every proof assistant" without that caveat is misleading.

There is also a problem with LAWS.bend. The typechecker only guarantees that your code satisfies what's written in LAWS.bend — not that LAWS.bend says what you actually meant. There is nothing to stop an LLM from "satisfying" a law with a vacuous or narrower-than-intended formalisation — the trust problem simply shifts from the code to the specification (which could be also generated by LLM, and therefore incorrect). The repository even admits that the compiler itself is 99% LLM generated and not yet fully audited, which seems a questionable basis on which to build a "mathematical guarantees" marketing.