41–50 of 105 posts
> There are no variable names. @Int.0 is the most recent Int binding; @Int.1 is the one before. You already lost me here. There's a reason variable names are a thing in programming, and that's to semantically convey meaning. This matters no matter whether a human is writing the code or a LLM.
Agreed.
I'm working on a language designed for machines to write and humans to understand and review.
It doesn't seem worthwhile to have code nobody can understand.
> There are no variable names. @Int.0 is the most recent Int binding; @Int.1 is the one before. You already lost me here. There's a reason variable names are a thing in programming, and that's to semantically convey meaning. This matters no matter whether a human is writing the code or a LLM.
Earlier quoted context omitted.
Presumably an analyzer that makes it an error to not have an immediately traceable zero check. C# can do something similar with null references. It can require you to indicate which arguments and variables are capable of being null, and then compiler error/warning if you pass it to something that expects a non-null reference without a null check.
But that’s because null is a static type. Zero isn’t a static type. How can I know if a calculation produces zero if I can’t predict the result of it at compile time?
The problem is these checks can be rather slow and people don’t want to wait a long time for their type checking and analyzers to finish. But LLMs can both wait longer and by internalizing the logic can reduce the number of times it will need to trigger them.
Edit: I’ll need to examine this project to know where (or if) they draw the distinction between normal type checking and a post type check analyzer. If they blend the two and throw the whole thing into Z3 it’ll work but it’ll be needlessly slow.
Edit: What I’m calling a post type check anyalizer they’re calling a contract verifier and it’s a distinct stage with ‘check’ (type check) then ‘verify’ (Z3).
This is exactly the wrong approach. LLMs are good at writing programming languages they already know, that are well represented in the training data, not at writing programming languages that they have never seen before, so that you have to include the entire programming language manual and lots of example code in every prompt.
Earlier quoted context omitted.
But that’s because null is a static type. Zero isn’t a static type. How can I know if a calculation produces zero if I can’t predict the result of it at compile time?
I think it's about if there's a possibility of it being zero. Of course there's no way to tell at compile time that a value will definitely be zero. So, in pseudocode int div(int a, int b): return a / b; Would probably be a compile time error, but int div(int a, int b): return b == 0 ? ERR : (a /b); Would not, or at least that's what I'd expect.
Yes there is. Dependently typed languages like Idris can inspect terms at the value-level during compile time. Rather, instead of proving that the divisor will be zero, you must instead statically prove that the divisor cannot be zero; otherwise the code will not typecheck.
Earlier quoted context omitted.
I think it's about if there's a possibility of it being zero. Of course there's no way to tell at compile time that a value will definitely be zero. So, in pseudocode int div(int a, int b): return a / b; Would probably be a compile time error, but int div(int a, int b): return b == 0 ? ERR : (a /b); Would not, or at least that's what I'd expect.
> Of course there's no way to tell at compile time that a value will definitely be zero. Yes there is. Dependently typed languages like Idris can inspect terms at the value-level during compile time. Rather, instead of proving that the divisor will be zero, you must instead statically prove that the divisor cannot be zero; otherwise the code will not typecheck.
int integer_division(int a, int b) { if (b!=0) return a/b; raise(SIGFPE); }
Great.
> The empirical literature shows that models are particularly vulnerable to naming-related errors like choosing misleading names, reusing names incorrectly, and losing track of which name refers to which value. I think Vera might be missing something here. In my experience, LLMs code better the less of a mental model you need, vs the more is in text on the page. Go – very little hidden, everything in text on the page…
> The empirical literature shows that models are particularly vulnerable to naming-related errors like choosing misleading names, reusing names incorrectly, and losing track of which name refers to which value. I think Vera might be missing something here. In my experience, LLMs code better the less of a mental model you need, vs the more is in text on the page. Go – very little hidden, everything in text on the page…
> The empirical literature shows that models are particularly vulnerable to naming-related errors like choosing misleading names, reusing names incorrectly, and losing track of which name refers to which value. I think Vera might be missing something here. In my experience, LLMs code better the less of a mental model you need, vs the more is in text on the page. Go – very little hidden, everything in text on the page…
> But writing Haskell, it's pretty bad, I’m surprised by this. Most likely significant white space is a big part of the problem (LLMs seem horrible at white space). Functional with types has been a win for me with Gleam.
> The empirical literature shows that models are particularly vulnerable to naming-related errors like choosing misleading names, reusing names incorrectly, and losing track of which name refers to which value. I think Vera might be missing something here. In my experience, LLMs code better the less of a mental model you need, vs the more is in text on the page. Go – very little hidden, everything in text on the page…
"No LLM has ever been trained on Vera. There are no Vera examples on GitHub, no Stack Overflow answers, no tutorials — the language was created after these models' training cutoffs. Every token of Vera code in these results was written by a model that learned the language entirely from a single document (SKILL.md [https://veralang.dev/SKILL.md]) provided in the prompt at evaluation time."
If LLMs do much better with Vera (or something like it) than with traditional languages, we may be entering a time when most machine-written code will be difficult for humans to review - but maybe that ship has already sailed.