alt Hacker NewsBend – A language that blocks AI mistakes via proof, on CPU and GPU
Comments
claude: 1 commit 1,722,119 ++0 --
Why would anyone want to work with such a dystopian setup? Prove your code directly in Lean or Coq or leave it.
How is that better than just writing tests and running them in any other language, let's say Go?
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?
Not the AI slop background colour T_T
Awesome! Now we can use AI to manage our nuclear defense and attack response.
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.
A single commit in github, and the compiler isn't there anyway. Where is the compiler?
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.
[flagged]
[flagged]
[flagged]
[dead]
[dead]
[dead]
[dead]
[dead]
Great team behind it. SSL cert is quantum resistant even.