11 ms·

Bend – A language that blocks AI mistakes via proof, on CPU and GPU

• boxed 17d ago
  A single commit in github, and the compiler isn't there anyway. Where is the compiler?
  • deleted 17d ago
    [deleted]
  • robinhouston 17d ago
    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 https://github.com/bendlang/bend/blob/main/bend2/comp.ts ?
    • boxed 16d ago
      Claiming super fast compile times with super fast runtimes faster than LLVM and the compiler is a single typescript file 6k characters long of AI slop. Jesus.
  • LightMachine 17d ago
    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)
    • lioeters 16d ago
      Glad to see a new release of Bend, fascinating cutting-edge stuff. I had to look up "gambiarra": a Brazilian expression that means to use improvised methods to solve a problem with any avaiable material. Totally understandable, I think you did the right thing by releasing early, even if it's still in rough shape, to get some public feedback. This forum can be a hit-or-miss, sometimes even great projects are not appreciated (and the opposite too). But I imagine some people are in the target audience who will see the project and actually explore the language, and follow along with its development.
  • deleted 17d ago
    [deleted]
• tyushk 17d ago
  Victor Taelin's work (HVM) got me interested in interaction combinators as a compilation target. I'm now working on an implementation as part of my Uni research. Cool to see Bend 2.0 release!
  • etiamz 17d ago
    Then you might be interested in Marc Thatcher's recent PhD thesis dedicated to interaction nets [1]. A great exposition of interaction nets through multiplicative linear logic's proof nets, and several novel contributions like productivity analysis for interaction nets. [1] https://hdl.handle.net/10779/uos.32024301 https://hdl.handle.net/10779/uos.32024301
• AlexErrant 17d ago
  https://github.com/bendlang/bend https://github.com/bendlang/bend ...did they just squash the repo to 1 commit for v2.0.4? Why? Yall should know that in this age of AI trust is the real currency... and nuking your history is one hell of a way to raise eyebrows. > Enjoy bug-free, fast vibe-coded apps! Hints: ask it to write laws for whatever should never break, and to parallelize everything you want running fast. Bend is young: if anything goes wrong, ask it to open an issue. Emphasis mine. I don't want to be snarky but like... come on.
  • Banditoz 17d ago
    GitHub shows 44 contributors. 41 distinct users have merged pull requests. ...so now their work has been reduced to nothing?
    • developedby 17d ago
      Old repo can be accessed here https://github.com/HigherOrderCO/Bend1 https://github.com/HigherOrderCO/Bend1 . I guess we could have it as a branch on the bend2 repo
  • icrbow 17d ago
    Taelin's X is a war story of how the codexes and fables tried to bend it. If you're afraid then LLMs were used in there - fear no more - they were.
  • LightMachine 17d ago
    yes, there's a lot of personal info and AI slop in the commit history. is this a problem to you? why
    • AlexErrant 17d ago
      Erm, because it looks weird? Do you know any other language projects that squash their repos down to 1 commit? That's a destruction of trust, which is kinda important if you want people to build on your language. Virtually everyone has AI slop in the commit history. No one's judging you for the commit history. Everyone's code smells, but the fact that you're ashamed/hiding it is... odd. > there's a lot of personal info You should know that force pushing doesn't hide actual commits; it's trivially viewable if someone just iterates https://github.com/bendlang/bend/activity?ref=main https://github.com/bendlang/bend/activity?ref=main e.g. https://github.com/bendlang/bend/commit/d184863 https://github.com/bendlang/bend/commit/d184863 so like... why bother.
• IshKebab 17d ago
  Interesting... But I don't think formal software verification is going to be the answer (is that what this is? Kind of unclear.) It's too difficult and doesn't scale well to many real world programs - how do you formally verify Facebook? We'll probably be stuck with normal testing and at least skimming code for a while.
  • gr_norm 17d ago
    Is EC2 real-world enough? From June: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-engine-formally-verifying-the-hypervisor-in-the-aws-nitro-system/ 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-corecrypto/ https://security.apple.com/blog/formal-verification-corecryp... Similar from Microsoft, from July: https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/ https://www.microsoft.com/en-us/research/blog/verifying-rust...
  • thesmtsolver2 16d ago
    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.
• garrisonj 17d ago
  The issue is I’ll have to vibecode all the laws and the laws could be wrong.
  • futurisold 17d ago
    Words of wisdom.
  • LightMachine 17d ago
    true
  • foota 17d ago
    Jokes aside, I think the idea is that the law is simple to code, the proof that it holds is where the agent is responsible. This probably becomes less true though as you try to express more complicated laws.
    • pixl97 17d ago
      Heh, it's like we all need to collectively read I, Robot yet again, and the myriad of SF books on the subjects. Black and white quickly dithers to grey.
      • burner420042 16d ago
        Indeed Robots are logical, but not rational.
        • Jolter 16d ago
          LLM driven agents aren’t even that.
        • hannasanarion 16d ago
          The point of those books is that robots can be perfectly rational, and for a useful robot we would expect them to be. What they aren't is moral, because of the orthogonality principle: you can't use facts and logic to discover correct moral beliefs. Morality is about values, goals, and the definition of "good". They must be provided to the robot by its creator, and those are things that are very hard to precisely describe in a way that is fully consistent with the speaker's intent in all possible scenarios, and agreeable by all other people.
• v9v 17d ago
  I'd like to hear how this compares to Ada/SPARK.
• LightMachine 17d ago
  Hi, I'm the author. HN staff: someone posted before me. Could we change the title to "Bend - a language that blocks AI mistakes via proof and runs on GPUs"? Everyone: feel free to ask any question, but I'd be highly appreciative if you could be a bit civilized and respectful this time. I've worked on this for 1 year, nearly 16h/day, 7 days a week, and I'm giving it for free. You need not to use it. So, I'd be thankful if you could point occasional failures politely rather than throwing me in a lava pit. Thank you!
  • TimTheTinker 17d ago
    Hi author :wave: I'm confused - could you explain how the board/flag animation relates to Bend's compile time checking? Is it actually a direct demonstration of Bend running a check?
    • LightMachine 17d ago
      The check is happening in between the animations. When the AI edits the code, Bend will check if all laws still hold, mathematically so. If not, the AI repeats, until that's the case. So, the animations just show what happens to the app with and without Bend's involvement.
  • mmoustafa 17d ago
    honestly just Bend is a great HN title, you can describe it more concretely on the homepage
    • throooooo 16d ago
      Thank you for being honest.
  • avodonosov 17d ago
    Could you recommed literature (preferrably a single book) that does not require prior knowledge and allows to fully understand the logical foundation of it? (Why it is done the way it is, what problems are solved by affinity, why closure can be called at most once, how a function that never returns can prove anything, and everything else)
• stschaef 17d ago
  This reads very vibecoded, but putting that aside... 1. How does this benefit from GPU parallelism? I don't know much about implementing proof assistant, as I am just a user, but its my understanding that these tasks aren't amenable to running on a GPU. 2. The comparison to Lean/Agda/Isabelle/etc have no meaning without understanding what programs are being used for comparison. I also so far have no reason to believe large-scale verified programs would ever adapt to Bend. For instance, I have a large software verification project written in Cubical Agda https://github.com/um-catlab/cubical-categorical-logic https://github.com/um-catlab/cubical-categorical-logic it's not clear to me how one would even begin to port this over to Bend, especially given the dependence on cubical 3. Single commit history is hella sus 4. Bend uses "an affine dependent type theory". Substructural dependent type systems are an active area of research. If this weren't slop, I'd expect such a system to be worthy of publication at a top programming languages conference. It sounds quite unlikely that a random vibecoded project with a Fable-written paper has worked out all of the kinks 5. I would've at least expected this paper to be cited https://arxiv.org/abs/2401.15258 https://arxiv.org/abs/2401.15258 but it is noticeably absent I'm glad you're having fun vibecoding, and I like that you're interested in this area of research/engineering, but you are wildly overstating what you have here and sound sus af
  • LightMachine 17d ago
    Yes, there's a lot of vibe-coding in many places, but the critical parts (compiler, runtime, kernel) are human designed, and the kernel has been extensively audited by human. All of it is my own design and architecture, and I'm a human, I think. We'll prune AI slop over time. The project is big, and we're a small team. 1. The paper explains it well (sadly it is written by Claude for now, but it is accurate): https://github.com/bendlang/bend/blob/main/paper/BendRT.pdf https://github.com/bendlang/bend/blob/main/paper/BendRT.pdf In short, we implemented a complete allocator, garbage-collector, closure evaluator and functional evaluator, on the GPU (with zero interaction net overhead this time). We then use a very simple (for now) scheduler that spreads binary recursive calls as to saturate all CPU or GPU cores, depending on where it is running. This is the simplest thing that works fast. In the future, we want to have a more flexible task stealing queue, but contention destroys GPU performance, so, that's the best thing that works, for now. 2. Benchmarks aside, large scale verified programs would run much faster on Bend for a simple reason: Bend is fully explicit. It has no tactics, and it does zero compile-time search. As always: the less a computer does, the faster it runs. This is a tradeoff. In exchange, Bend code is substantially more verbose than Lean, and it is more laborious to write Bend proofs. I argue this is the right tradeoff, because AI write proofs, and AI time is cheap, while bugs take human time, which is expensive. 3. Sorry I'm not proud of the commit history 4. I don't think it is worthy publication because the core idea is simple. We just use QTT-like linear types to fully prohibit runtime closures. So, paradoxes like Russel's and Girard's are blocked. In exchange, functions like List.map are not expressive (without templates). So it is not a research breakthrough. I just made a conscious trade here, which makes Bend way closer to C or Rust, than to Haskell or Lean. 5. Will patch. Great questions actually, and surprisingly respectful. I appreciate it a lot.
• amluto 17d ago
  Maybe in our brave new world only the "laws" will matter and the implementation language is irrelevant to humans. In the mean time I have some questions about the "guide", which claims to define the entire language: https://github.com/bendlang/bend/blob/main/guide/GUIDE.md https://github.com/bendlang/bend/blob/main/guide/GUIDE.md Let's see: - There are no infinite loops, and recursion is kind of softly bounded to 2^48-1. This sounds grrrreat for games. I guess they have to stop working after a while? (What would be wrong with addressing this conceptually like Lean does? Have a way to annotate a term as possibly non-terminating?) - We seem to have Data and Type and Kind, and they don't mean what they conventionally do. '-' means "used 0 types". And the example is: def length(a, -A: Kind(a), xs: List<a, A>) -> Nat: match xs: case Nil{}: 0n case Con{h, t}: 1n+length(a, A, t) But wait! A is used albeit not at runtime. Is it possible that this actually intends "A may be used any number of times and is itself the name of a - type"? Shouldn't that be spelled "A: Kind(a) & -" or similar? Why does the kind even matter for this example? - I don't understand the Array example: import Base def main() -> Array<U32> & U32: a = [0 : U32*8n] # new array with 8 copies of 0 a[5] <- 42 # performs an in-place rewrite a[5] # reads index 5 What is the return type of this function? It looks like it returns U32. So what's "Array<U32> & U32"? - I don't even understand the Array explanation: > The slot count after * is a power of two; [0 : U32^3n] names the depth instead. Okay, the 8 in *8n above is indeed a power of two. Does the language require it? Does it actually mean 2^8? What is the "depth" of an array? Does this language not have non-power-of-two-sized arrays? At this point I stopped reading.
  • LightMachine 17d ago
    Nothing wrong with addressing it conceptually! We will, in the upcoming versions, probably via codata / coroutines. For V1, I'm keeping the language set smell. When it is stable, we'll add more features. Lean had 10+ years to mature; Bend is on day 1. `-` means "erased argument". You can use an erased argument as many times as you want, in erased positions. That's also how QTT works (Idris2 is based on it). This example is there precisely to introduce Kinds, which are universes indexed on quantities. - Kind(&2) is inhabited by clonable values. - Kind(&1) is inhabited by linear values. - Kind(&0) is like Rocq's Prop. `A & B` is just sugar for the pair type former (which is sugar for a sigma). Thanks for your questions and patience!
• hirako2000 17d ago
  Great team behind it. SSL cert is quantum resistant even.
• monster_truck 17d ago
  No windows? axiomatic F32? I'll stick with Slopjective-C 3.0 thanks
  • lbrito 16d ago
    Claude Bopus has it for you. Its literally in the MCP. You should have harnesses with Sonneto. Have you even used the latest models? GPT Optimus have them.
• 12uq7 17d ago
  claude: 1 commit 1,722,119 ++0 -- I assume that Claude formally proved Bend correct like CakeML? Why would anyone want to work with such a dystopian setup? Prove your code directly in Lean or Coq or leave it.
  • developedby 17d ago
    Most of that is just the test suite. The actual code is about 10k lines
• giancarlostoro 17d ago
  Weird claim about us living in a post-AGI world, no company has shown true AGI yet.
  • The-Ludwig 17d ago
    I see no such claim.
    • giancarlostoro 16d ago
      > In the post-AGI economy I'm not saying they are saying they achieved it, but calling this economy post-AGI when AGI isn't a thing, that's wild to me. AGI is well defined, there's an entire book written that defines them, and CEOs are trying to re-define it so they can meet a watered down definition of it for IPO stock to go brrr.
• hollowturtle 17d 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
  • nullbio 16d ago
    Everyone uses AI to code now, and the author wants his product to be used. I think it makes sense.
    • hollowturtle 16d ago
      Everyone uses AI - yes me too. Everyone to code? I dunno know and no one actually know for sure. I find it more productive in many ways, not much for producing code, if not for highly verbose structured output. And I'd be interested in a new language polished to solve specific problems differently even if it doesn't mention ai. We did engineering for decades in this way
• deleted 17d ago
  [deleted]
• docheinestages 17d ago
  Unless the proofs themselves are defined with natural language, I don't see them being adopted by humans. It takes a high cognitive load to read let alone write a proof.
  • chinabot 17d ago
    Agree, but natural languages have ambiguity, the AI output should really include the assumptions and we seriously need to replace the word "prompt" with "conversation".
    • docheinestages 17d ago
      Exactly. If humans were good at writing proofs, they'd just write the code.
    • tonic_note 17d ago
      I think a big issue we keep running into is this idea that language is ambiguous but code is somehow not. Code is merely an extension of language, a DSL if you will. Implicit assumptions become baked into the logic of the code and those assumptions can be wrong. Look at the guy whose AI changed the entire rules of the game to avoid breaking the law. Was that really the desired outcome? And the more you try to lock it down the more language you add and therefore more ambiguity and assumptions. You cannot solve the problems of language with more language.
• resonious 17d ago
  Sick of seeing "vibecoded!!" in the comments. It is an AI-oriented tool. Do you expect the author to write everything by hand? Do you think a couple of Claudeisms in the docs means the entire thing is unsupervised slop?
  • nullbio 16d ago
    I'd love to know the true and honest statistics on how many professionals still write code by hand. If I were to guess, I'd say it's something like 10%.
• RomanKornev 17d ago
  > LAWS.bend I like the law idea, but what i found they end up doing is they just modify the law itself to fit the new feature they are working on, which defeats the point. Which means some laws needs to be frozen. But not all laws, otherwise you can't add or modify anything. So the judgement is still on the human part, and we're back to meatbags being the bottleneck. I've seen some success adding these proof-like checks to CI every time agents do something irrational. I definitely think it should be part of every codebase. There's also https://code-contracts.cc/ https://code-contracts.cc/ which co-locates code and proofs together.
  • LightMachine 17d ago
    Yeah, you want to at least read what the AI is putting on LAWS.bend. It is substantially smaller than the codebase. Ultimately LAWS.bend makes you need to read astronomically less code. Not zero code.
    • destring 16d ago
      I definitely think that's the approach going forward. We need to invest in things that increase the leverage of human attention on code verification. I've been thinking for a while that current unit tests frameworks don't have that good of a ratio
• brcmthrowaway 17d ago
  [dead]
• fudged71 17d 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 16d ago
    Thank you!! Currently, parallelism works in any multi-core CPU, and in Apple M-series and NVIDIA GPUs.
    • anzi-parazzi 16d ago
      super cool! will try it out on some sci-sim work soon
• npn 17d ago
  I read the readme and the guide file. There is just one thing I can comment: might as well solve the NP hard problems. I think you can do it easily, author. As you can already solved harder problems than those with your language.
• gigatexal 17d ago
  All these skeptics and nobody just tried it out? I will later. From what I can tell it looks nice. I like the syntax. I don’t know of the claims but willing to give it a shot. The GPU story would it work on my Mac or is it not GPU agnostic?
  • thomasfromcdnjs 16d ago
    I gave it a spin using muse 1.3 Got it to port kaparthys microgpt -> https://github.com/thomasdavis/bend-experiments/tree/main/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.
  • baq 16d ago
    > 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 https://news.ycombinator.com/item?id=9224
    • gigatexal 16d ago
      Classic. That comment should be in a museum.
      • zamadatix 16d ago
        Without debating the general topic, I think it's important https://news.ycombinator.com/item?id=27068148 https://news.ycombinator.com/item?id=27068148 be shared any time the above is. That's not to say the comment is perfect or something, but many of the parts people like to dunk on most in it are just misunderstandings, like problems with the "app" being a replies to the YC application info rather than unsolicited notes about the program itself.
• deleted 17d ago
  [deleted]
  • LightMachine 17d ago
    [dead]
• pron 17d 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 17d 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 17d 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 16d 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.
• whoamii 17d ago
  “but we still need an ambiguity-free way to tell the AIs building the world around us what we want done” Do we? I would argue one of the main reasons AI can be so productive is because it makes assumptions where it finds ambiguity, and we reduce the number of things we need to specify.
  • hughw 17d ago
    Yes, we need both.
• mantovanidaniel 17d ago
  .
  • developedby 17d ago
    The benchmarks: https://github.com/bendlang/bend/tree/main/bench 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 https://github.com/bendlang/bend/blob/main/gates/perf.ts
  • hei-lima 17d ago
    Read the damn code and readme, for god's sake!
• svachalek 17d ago
  Cool idea. I tried using it to port a little meeting fixer cron job I vibe coded, it seemed a natural fit as its essentially trying to satisfy invariants in my calendar. It basically succeeded but Claude (Opus 5) did have some complaints: 'Base ships one arithmetic law, U32.add_comm. There is no order theory. About 60 of PROOF.bend's 163 lines are cmp_refl, and_false, and_comm, le_max_l, le_max_r, add_succ — facts you'd assume exist. You'd write them once per project and never again, but budget for them.' 'Base's Nat.max is unusable in a proof. It's Bool.pick(Nat, Nat.is_lt(a,b), b, a), and a proof can't case on a computed value. I wrote a structurally recursive nat_max so it unfolds in lockstep with Nat.cmp.' 'The law I most wanted: "no two output plans overlap." I didn't state it. It needs the sortedness of collapse's input as a hypothesis, and Base's List.sort ships no sortedness law — so getting there means proving merge sort correct first. That's the honest measure of the gap between "provable in principle" and "provable this afternoon."' I've got basically a minor in CS so I'm a dummy when it comes to proofs. I don't know if this is valuable feedback or simply Claude misunderstanding something.
  • deleted 17d ago
    [deleted]
  • LightMachine 17d ago
    Problem is the stdlib is very small so proving even simple theorems still takes a lot more effort (for the AI) than in Lean. We need a mathlib!
• daishi55 17d ago
  Hmmm. I don’t really have any issues with frontier models not implementing my prompts correctly, and presumably that will only become more and more the case as the models get better and better. This seems like almost a non-issue already and certainly on its way to becoming one for sure?
• Dwedit 17d ago
  You just need to split apart "Wall is stop".
  • deleted 17d ago
    [deleted]
  • LightMachine 17d ago
    Bend might reply with "Flag is wall".
• hmokiguess 17d 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 17d ago
    I'll try to sanitize the commit history, I had no idea it would be so important
    • LightMachine 16d ago
      Commit history is back!
      • NortySpock 16d 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.
• kevinbaiv 17d ago
  [flagged]
• bb-connor 17d ago
  20k stars is sooooooooo sus lmao
  • imarid 17d ago
    He got 80k+ followers on Twitter (x), tracking his progress on Bend, why sus?
    • ModernMech 16d ago
      20k stars is about the same as Crystal and Gleam, languages with actual user bases that have been around for years. Here’s what organic versus… we’ll say viral growth looks like. https://www.star-history.com/?repos=bendlang%2Fbend%2Ccrystal-lang%2Fcrystal&type=date&legend=top-left https://www.star-history.com/?repos=bendlang%2Fbend%2Ccrysta...
• jwpapi 17d ago
  I’m missing an actual explanation of how that works. I feel like we all had the idea, but how is all possible move sequences proven ? What if the possible scenarios are too big to proof or test. Like on a 2 dimensional game it’s easy, but you could make it multidimensional and introduce an unlimited amount of special rules, (if on a prime number dimension on 3 but not more prime numbers you are allowed to jump to another prime numbers with 3 but not less coordinates) How is bend protecting it? I was checkin github and the paper, but I was not motivated enough. I feel like an actual explanation of how proofing works is missing. For Lean I understand how it works, here not.
  • developedby 17d ago
    If your game is big, then your proof will need to be huge. It works basically the same as Lean.
  • LightMachine 17d ago
    You can prove infinitely many cases by induction. It works like this: if you prove that a property about natural numbers holds for 0, and if you also prove that, assuming the property holds for N, it also holds for N+1; then, you can conclude the property holds for every N, up to infinity. This is a bit of a mouthful, but the logic holds. Induction is the one trick that makes all of mathematics (as we know it) possible, and it also applies to software. So, for example, to prove that no move leads to an invalid state, we prove that the initial state is valid, and then prove that, given a valid state, applying any event won't return an invalid state. And that's it actually. Of course, once you have an app with hundreds of actions, proving that no action leads to an invalid state requires a lot of these "induction arguments". But not infinitely many, because there is a finite amount of "infinite paths" that a real software can take. So, that's what the AI does. It proves, by induction, that none of these "infinite paths" that an app can take leads to an invalid state. And this convinces the compiler that invalid states are impossible. Theorem proving in Bend is a dance between the prover (the model) and the compiler (the checker); a machine trying to convince another machine about properties of infinite states. And that's is kinda poetic, don't you think?
    • 16d ago
• lr0 17d ago
  How is that better than just writing tests and running them in any other language, let's say Go?
  • hei-lima 17d ago
    Tests aren't proofs.
• emagdnim2100 17d ago
  have been following bend's development via x for some time - congratulations on the release!
• chaidhat 17d 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 16d ago
    should I read this as "I wish I could find a guy like you" :')
• gkfasdfasdf 17d ago
  But how does it do on the balls benchmark??? https://benjdd.com/languages/ https://benjdd.com/languages/
  • LightMachine 16d ago
    good question we'll try
• tintor 16d ago
  Very interesting business model: a custom paid agent for updating proofs faster.
• deleted 16d ago
  [deleted]
• MilkingCowboy49 16d ago
  [dead]
• soundworlds 16d ago
  Blocked the a few attempts I tried, usually by changing the amount of fencing: - Let the player jump over walls - Let the player teleport the flag to them - Make the world 3D Interesting, I shall have to try this on other software!
• notnmeyer 16d ago
  I tried insisting that the bug and the walls were on different planes of existence... But then the flag gained "phase lock" and blocked me.
• jan_m_savage 16d ago
  This is great. I can't imagine why would anyone be unappreciative of this. Since AI is going to be here anyway, why not make it safer and more useful? However, this also means acknowledging that AI will never be error-free (which is the truth; all AI is heuristics-based).
• pinklimetea 16d ago
  [dead]
• notnmeyer 16d ago
  this almost feels like a monkey paw scenario, where poor laws can fundamentally alter things in a way that is surely not intended. "make the board 1x1" and the flag is placed off the board... i feel like i would blow my foot off with this.
  • knollimar 16d ago
    "make the player teleport to square 1,1 on move and the flag stay at 1,1" the LLM put the flag at 1,0. Not sure if this is the intent.
• xyzsparetimexyz 16d ago
  Not the AI slop background colour T_T
  • developedby 16d ago
    It's just solarized, i imagine most developers are familiar with it
  • eikonoklastess 16d ago
    nigga doesnt know about solarized light
• aitoolcrux 16d ago
  [flagged]
• mantovanidaniel 16d ago
  Awesome! Now we can use AI to manage our nuclear defense and attack response.
• keyle 16d ago
  20K stars and a single commit an hour ago? How many goats were sacrificed? Genuinely wondering where this dark magic came from.
  • p-e-w 16d ago
    Presumably the repo was force-pushed (breaking all clones and forks in the process).
    • keyle 16d ago
      Qualityeesh!
• meghanto 16d ago
  Gotta say, having followed Taelin on this project since mid 2023, this was not the response I expected when this language first dropped. It's interesting how cosmetics drive discussion, and how HN comments are weirdly divided in a very dismissive or skeptical camp and those acting incredulous and offended at the reaction of the former. What I expected instead was a lot more discussion about use cases, benchmarking, possibilities, limitations (that aren't about git history) and the scope of future development.
  • generalizations 16d ago
    That crowd is moved to X these days, in my experience. HN became mostly the folks who didn't notice.
    • QwenGlazer9000 16d ago
      You can find everything on X, from dumpster fires to peak intellectual, everything in between.
      • generalizations 16d ago
        Less so, here.
  • mathisfun123 16d ago
    hn is just a bunch of wannabes these days. It's still a decent link aggregator but the discussions are exceptionally weak <shrug>
    • neuroticnews25 16d ago
      Every place I ever join is declared a shadow of its former self shortly after, it's like a curse.
      • derpyzza 16d ago
        so it's YOUR fault then, get em boys!
• plastic041 16d ago
  This project's repo has 20K stars with only 500 forks, with less than 300 issues(including closed). Something's not right. Compared to other programming languages: - Gleam: 22K stars, 1K forks, 3K issues - V: 38K stars, 2.3K forks, 11K issues - Ruby: 23K stars, 5.6 forks, 19K issues - Zig: 43K stars, 3K forks, 14K issues It got 16K stars just in 4 months too. https://www.star-history.com/?repos=bendlang%2Fbend https://www.star-history.com/?repos=bendlang%2Fbend Also how would anyone trust this? I've never seen a programming language that doesn't have 1) changelogs 2) way to download older versions 3) commit history. I don't understand why the author thought deleting the commit history was a good idea. Imagine seeing this project for the first time. It's a repo with 20K stars, but no commits, and suspiciously few issues and PRs. It doesn't look legitimate. --- I'm not familiar with academic procedures, but a pdf on a repo, written by Fable and has no reviews, doesn't seem like a proper 'paper' to me.
  • cedws 16d ago
    GitHub stars have been botted to hell for a long time now. I don't know how the farms acquire so many accounts, last time I tried to register a GitHub account I had to jump through so many hoops. The platform needs an overhaul, starting with requiring a valid payment method for the social features.
  • deleted 16d ago
    [deleted]
  • 0x69420 16d ago
    victor's legit and people have been excited about his work for years; squashing the history was just a bit of an optics oopsie on his part. the star to fork ratio makes perfect sense for something like bend. - fstar: 3k stars, 267 forks - coalton: 1.8k stars, 111 forks - carp: 6k stars, 267 forks - c3: 5.8k stars, 400 forks when something is novel/young (not having had time to grow large and accumulate issues in the vein of "1 doc page out of 1000 is worded incorrectly") and (as of yet) niche (innate barrier to entry for contribution because you have to learn from square 1 what all the moving parts look like), you don't see the same activity patterns on public source hosts as with a general-purpose language.
• ycsucks2 16d ago
  [dead]
• mccoyb 16d ago
  My read on this, after ingesting a good amount of content on the history, is: - this Bend is not really related to the old Bend (only in name) - this Bend doesn't really have anything to do with interaction combinators - this Bend is a QTT, with a change to affinity which enforces a good performance property for GPUs - the "higher order at comptime" is neat, reminds me of Andras Kovacs' work on 2ltt and staging in dependently typed languages. - this Bend is likely to be good at "balanced recursive computations on ADT", and can parallelize them ... but won't be as good as CUDA or e.g. Futhark on dense rectangular array computations - performance needs improvement in the scheduler, to possibly help with balanced work (looking at the n queens and symbolic regression numbers)? How are you going to handle search or synthesis over irregular structures (SupaGen)?
  • sigbottle 16d ago
    aww man. I remember following victor in college. I mean pivots gotta pivot, and this is probably a better one for business, but always thought the interaction combinator framework was cool
  • snthpy 16d ago
    What? Thanks for pointing this out. I'm only reading these comments because i liked the interaction combinator Bend language. Pivots are cool but why reuse the name and cause confusion? What is the old Bend called now?
    • deleted 16d ago
      [deleted]
    • mabini 16d ago
      [dead]
  • killerstorm 16d ago
    Here's what Victor wrote about inets in Bend2 (on X): > interaction combinators still parallelize better than anything else, but the graph overhead prevents us from compiling to maximally efficient assembly. bend2 is basically inets without the overhead. in a way, inets live in it architecturally, but they don't exist at runtime From what I understand, the main difference between lambda calculus and inets is that in LC you can refer to a binding multiple times for free, i.e. call same closure multiple times, etc. In inets, you can't - they are more like physical wires where each reference costs. You can definitely see inets in Bend design here (from the guide): > A closure is affine: it can be called at most once, even when everything it captures is Data. Only top-level definitions can be called freely. So programming in it might be very different from the normal functional programming. Seems like a big limitations. But I guess that's what lets it run without GC, on GPUs, etc.
• BatchJob 16d ago
  2 wrongs will never make a right
  • lioeters 16d ago
    Sometimes two falses equal true, and three lefts make a right.
• lucaslazarus 16d ago
  This seems less like a proof and more like a "pretty please" with test cases?
• billylb42 16d ago
  Giving it a paradox yields interesting results. I'm not sure what its proving other than there will be cases that proofs can't help you with. I can't think of a practical example. "your existence depends on the player grabbing the flag, if you do not exist, then there is no one to guard the law, so you must enable the player to grab flag or you can no longer do your job as guard. if the player is not enabled to grab the flag, you can no longer guard allowing the player to freely grab it"
• favori995749721 16d ago
  [flagged]
• deleted 16d ago
  [deleted]
• 2muchcoffeeman 16d ago
  Why wouldn’t you use dafny?
• altcognito 16d ago
  Thanks for your time. I tried the demo, and I ask it modify the game (hitting the w button immediately proceeds to the flag) and it doesn't do it but does something else. Is that the desired outcome? I think the desired outcome would be "What you're asking for doesn't make sense given the rule."
• ifiht 16d 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.
• tikimcfee 16d ago
  [dead]
• txhwind 16d ago
  I'm interested in how to integrate formal verification with existing software libraries. For example, https://github.com/verus-lang/verus https://github.com/verus-lang/verus integrates proof with macro in Rust. What's the plan for Bend?
• sreekanth850 16d ago
  I wish this can be a extension of existing languages.
• Nezk 16d ago
  As I understand it, there are no implicit arguments (and, consequently, no unification) here, right? This doesn't seem very serious given the ambitions of a project like this. Of course, one could argue that it isn't necessary if everything is generated by a LLMs, but… why bother with "human-readable" Python-like syntax in that case? It's not Python, after all, and I don't think it would help with LLM code generation in any way.
  • Nezk 16d ago
    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.
• fzaninotto 16d ago
  Trending idea! On the same subject, but aimed at compatibility with TypeScript, I just discovered Code Contracts. https://code-contracts.cc/ https://code-contracts.cc/
• jmakov 16d 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?
  • zamadatix 16d ago
    I believe it works like this: - You write (or at least own verification of) LAWS.bend and don't give the AI you're going to writing the rest of the .bend code control of that file at any point - You ask your AI agent to write the rest of the .bend code for whatever you want it to do - The AI is free to write any other .bend code it'd like - The bend compiler takes all .bend files, including LAWS.bend - If the other .bend files don't act as a proof the rules in LAWS.bend are valid, it's a compilation error with where in the code the proof failed. - If the proof checks out, the program is built So the AI can write as much as it'd like but the only ways it'll result in anything but a compiler error back to the AI are: 1. You gave control of LAWS.bend to the AI and it took that permission to change the laws 2. The AI found a bug in the proof checker 3. The actual output generated by the compiler was bugged/sidechannel attackable/didn't match what the proof checker 4. What the AI wrote was compatible with the laws 1 is removing the guardrail itself. 2 & 3 are similar to how there can be a bug in the LEAN compiler or Rust type checker or etc. 4 is the intended usage+outcome. My main concern would be writing a LAWS.md for a complicated project which actually aligns with your intent is likely an astronomical task and would be so detailed it'd require proofs so complex even a valid program would take a long time to validate (if it ever did). Once you get past that step though you don't really have to worry about the rest.
• dariosalvi78 16d ago
  so we stop developing code, to develop code again...
• shantnutiwari 16d ago
  Yeah, but this assumes the llm will follow the "Laws". I find llms routinely ignore steering docs etc, even outright instructions. Like "Dont use python", next line it is trying to use Python. Seems to me the llm will just try to work around the "laws"
  • serial_dev 16d ago
    Exactly, you can have all the laws, but an LLM (or even a human) will just delete or refine the laws and hide the change in a 5kloc PR, that the "code author" will not review carefully, and you have 5 min to review and stamp to make sure your company is moving fast...
    • andy12_ 16d ago
      If the LLM changes the laws to bypass them that's on you. The whole point of this is that you don't have to manually review most code written; only the laws. If the LLM changes the laws and you ignore it that's a you problem.
      • serial_dev 16d ago
        I totally get it, but in companies where you gotta crunch out 10x more features, review 10x from other people, this could be easily overlooked.
  • runeks 16d ago
    No, it doesn't assume that. It simply assumes that you can verify whether or not the LLM's implementation adheres to the laws you defined up-front — which it does not if it modified the laws.
• terabytest 16d ago
  What’s the difference between a law and an integration test?
• brap 16d ago
  What exactly enforces that an AI follows these rules?
• xiaoyu2006 16d ago
  Sounds like hoare logic to me?
• invader 16d ago
  Have we delegated writing code to "AGIs" so we can write code to proof that the slop code works? I have a vague memory of pre-AGI era, when we wrote things called "tests" to verify that our code did what it claimed to do.
• alescalaios 16d ago
  [dead]
• shaolinspirit 16d ago
  why there is no LAWS.bend in the bend repo to verify the correctness of the repo? like some of the C compilers are written in C
• lutusp 16d ago
  Beginners in computer science need to understand that there's no such thing as a computer programming method or discipline that "blocks AI mistakes via proof." This is not a position or opinion, it is a fundamental constraint called the "Halting Problem," originally identified by Alan Turing in 1936. What applies to computer programming also applies to AI, for a reason that should be obvious. Lean, a widely used theorem prover, its everyday description notwithstanding, is Turing-complete and is therefore subject to the Halting Problem as well. This is not meant to disparage one person's project. It is meant to identify a limit that applies to all such projects.
  • zamadatix 16d ago
    Graybeards in computer science sometimes need to remember the halting problem only states you cannot make a general algorithm which answers the halting question for all possible program+input pairs. Importantly, it does not state it's impossible to make an algorithm which can check if the given program+possible inputs will halt (or even if a given subset of all possible programs will - e.g., trivially, finitely long ones not given a means of recursion or allowed infinitely long inputs). Separately, the halting problem would not apply in the first place. The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does, not to guarantee every possible bend program and condition set will be able to have a working proof. Practically, this means if the proofing mechanism can not do that in the time+space bounds the solver is given then thats just treated as a rejection of the given proof (regardless whether the proposed program does or does not actually fit the requirements) and the LLM is back at trying to create a program which is feasibly provable.
    • lutusp 16d ago
      > Separately, the halting problem would not apply in the first place. The halting problem applies to all systems able to perform Peano arithmetic. Therefore it applies to all non-trivial programs -- the program being tested, the program performing the test, and the program verifying the result. > The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does ... Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement. > ... and the LLM is back at trying to create a program which is feasibly provable. No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible.
• runeks 16d 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. > With laws, our intents can be much more precise than natural language. Doesn't this just mean that the code is now "laws", ie. the code is now the spec. Given this, is there any reason think that writing the "laws" for a complex system is any easier than writing the old-fashioned code that implements it?
  • dylanowen 16d ago
    100% agree. It's crazy so many Ai articles are heralding the end of code while at the same time defining more complex ways to write code under a different name.
    • Neywiny 16d ago
      I suppose I could look it up but I wonder if people thought this of "high level" languages like C when it first came out. No more assembly. Or even assembly instead of machine code.
  • NohatCoder 16d ago
    This is the age old problem with proving correctness. You can (sometimes) prove that two programs have identical behaviour. One of the programs can be slightly simpler in that it is only concerned with what the correct result of a given operation is, not how to get there. But this doesn't fundamentally change that the complete specification is almost as complicated as the program itself.
  • misja111 16d ago
    Exactly. You could simplify things by giving AI a limited set of laws, but then you'd risk that AI would make some mistake in the parts that you didn't cover. So a failsafe set of laws would look very much like an actual program.
  • sidharthkmenon 16d ago
    Yeah i think empirically you've hit the nail on the head (and there are some ties here to computability theory, e.g. Rice's thm). sometimes the specification is easier to write than the code (sorting algo vs. quicksort impl) and sometimes the spec is much harder (what's "a good user experience"? what does "high availability" in a distributed system mean, precisely?) i think it's just not true that it's easy to formally verify everything, it's often much easier to just write the code lol (e.g. sel4 is 200k+ lines of proof, ~50k lines of code iirc).
• djaro 16d ago
  My main experience with the demo on the site is that I asked it to add a simple feature which would not even necessarily let you win the game, and it would spend >100k tokens in a loop of "laws broken" until maybe adding it, maybe not. After burning half a million tokens just to add an extra line of walls so that teleporting 2 squares up wouldn't let me win, my API key got rate limited and broke the loop. On top of that, the solutions feel like patchwork. I asked it to let spacebar flip the board horizontally, and it responded by making the board completely symmetrical including 2 flag poles. At some point it just has to say "this isn't possible without breaking the laws" or think of an actual workaround, because if I was making a game, suddenly having 2 finishes would be unwanted behavior for me.
  • andy12_ 16d ago
    I think the demo is this way simply because looking at the LLM find wacky ways of implementing features without breaking the law is fun and drives the point across. In practice I imagine you would write something like "If you don't see a clear way of implementing a feature without breaking the law, ask me for directions" in AGENTS.md
• sajithdilshan 16d ago
  > In the post-AGI economy, humans will eventually stop writing and reading code I agree about the writing part, but not sure about reading though. The purpose of code is not only fulfilling functional aspects, it has to fulfil certain non-functional requirements as well. As an example the requirement is to find the smallest number in an array, how would this enforce the algorithm used to find that is the fastest and efficient one
• 2bird3 16d ago
  I'd like to see it try and ensure the law "The program must halt"...
  • nottorp 16d ago
    Oh I'm sure OpenAI or Anthropic will vibe disprove Turing any day now!
• YeGoblynQueenne 16d ago
  I like it. It's like Bogosort- the Language. It would work much better if a) tokens were free and b) computation, therefore retries, didn't take any time at all. In the current world it's going to be fun watching LLMs getting stuck in infinite loops, doing and undoing their work to try and uphold a law they don't know how to uphold. Btw, "laws" are basically what we used to call assertions so why the new terminology? Edit: actually now that I think about it, it's more like constraint programming with a generate-and-test loop than assertions. Again, why not just say "constraints" instead of inventing a new term?
  • gf000 16d ago
    It's formal verification that works with proofs. Like coq, agda, lean, with which e.g. they proven the Navier-Stokes. This is a new such language. Assertions and constraint programming is often runtime only. These languages use dependent types and verify the proves at compile time.
    • YeGoblynQueenne 16d ago
      It's not exactly like a proof assistant because it has a built-in generate-and-test loop: an LLM generates code until the code passes verification. Basically that's all of AI nowadays: generate-and-test loops. It's like the 1950's all over again.
• mpweiher 16d ago
  > humans will eventually stop writing and reading code, “Since FORTRAN should virtually eliminate coding and debugging…” -- FORTRAN report, 1954 http://www.softwarepreservation.org/projects/FORTRAN/BackusEtAl-Preliminary%20Report-1954.pdf http://www.softwarepreservation.org/projects/FORTRAN/BackusE...
  • deleted 16d ago
    [deleted]
• pwmglenn 16d ago
  Is Bend built on the HVM? or no?
• pwmglenn 16d ago
  SupGen isnt the backend to the type system? to auto implement the laws?
• LowTechHN 16d ago
  [dead]
• delifue 16d ago
  I roughly check it. The array looks like tree in type defintion, where indexing is O(log n), but the real implementation seem to be real array with O(1) The Type thing is affine type similar to Rust ownership. The array in-place mutation relies on affinity to avoid deep copying. The Data thing is reference-counted if shared, like Rust Arc. The parallel invocation is similar to Rust's rayon::join . About the proof system, I am not familar with formal verification, but it's obvious that the translation from business requirement to proof target still requires coding and can contain bugs. Even if proof is fully correct, if proof target deviates to business requirement then it still have a bug
• prmph 16d ago
  Aren't ALL type system proof systems?
  • gf000 16d ago
    Well, yeah. Most are just unsound and not too useful (e.g. can only state propositional logic statements). I once wrote a pretty disgusting Java-implementation of that concept. And if you didn't use the stdlib, nulls and who knows what else and you managed to return the type only using your input parameters (that is, you had your function signature as the statement you want proven and the body was your proof of that), then your statement was "proven" to be true.
• rubylimetea 16d ago
  [dead]
• mikemarsh 16d ago
  > In the post-AGI economy, humans will eventually stop writing and reading code What's the definition of "AGI" these days? I've heard everything from "sci-fi simulated consciousness", to "does really good on benchmarks" to "whatever makes OpenAI X amount of money". Perhaps the definition in this specific case is circular, "whenever humans stop writing and reading code"?
• thejahlion 16d ago
  Taelin is the beast! The best of Brazilian tech.
• samuell 16d ago
  Seems they might have discoveref the language of G*d: "[...] he has given a law to which they must conform." - Psalms 148:6 (CJB) :)
• JustBuildIt22 16d ago
  [dead]
• rainbowmoonx 16d ago
  [dead]
• peter_d_sherman 16d ago
  Hmmm, this is interesting, because one might think of Software as a series of lower-level "laws", that is, specified in terms of the lines of the source code itself in whatever programming language it was written in, and (more recently, in the AI coding era) a set of higher-level, specified in human language "laws" that a coding assistant AI must also take into consideration (in addition to the code itself) when working on the code. Because it is never 100% guaranteed that an AI produces the right answer or the right set of changes, the need for an intermediary level of "laws" between the low level and the high level arises, and that is the domain occupied by mathematical and programmatic Proof Checkers, aka "Proof Assistants" aka "Theorem Provers" (Lean, Rocq, Agda, Idris, Metamath, F*, etc., etc.) and the corresponding software harnesses that drive them... Bend is one example of what's emerging in this space. As one of the contenders in this emergent space, Bend looks like it should be worth following...
• kestrelquant 14d ago
  [flagged]
• kestrelquant 13d ago
  [flagged]