5 ms·

Vera: a programming language designed for machines to write

111 points by unignorant 5mo ago

hyperhello 5mo ago
> Division by zero is not a runtime error — it is a type error. The compiler checks every call site to prove the divisor is non-zero. Elaborate a little here.
- hgoel 5mo ago
  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.
  - hyperhello 5mo ago
    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?
    - hgoel 5mo ago
      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.
      - still_grokking 5mo ago
        Or it's just some AI brain fart… The whole things looks vibe-coded, and vibe-designed.
      - rdevilla 5mo ago
        > 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.
        hyperhello 5mo ago
        Okay, int integer_division(int a, int b) { if (b!=0) return a/b; raise(SIGFPE); } Great.
        rdevilla 5mo ago
        You don't appear to understand the difference between runtime and static analysis/compile time, or term-level and type-level.
        hyperhello 5mo ago
        Great! Explain it to us while I read to my kid!
        cjbgkagh 5mo ago
        The ‘let me google that for you’ is set to be replaced with ‘let me ask ChatGPT for you’.
        rdevilla 5mo ago
        Don't get mad because you're too lazy to even ask the AI. You are first to be replaced in the workforce. Or maybe it's over your head and you should just stick to reading children's fiction after all. Want some colouring books too?
        hyperhello 5mo ago
        Yes! We can always use more books and toys here!
    - cjbgkagh 5mo ago
      Post type check analyzers can work with more than just the type information, you can really do whatever you want at this stage. The normal highly optimized type checker handles the bulk of the checking and the post type check analyzers can work on the residual. You wouldn’t type check a file that doesn’t parse, and you wouldn’t run the analyzers on code that doesn’t type check. 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).
ginko 5mo ago
Is there any evidence that using structural references rather than names allows large language models to generate better code? This bit just feels like obfuscation for obfustcation’s sake.
- Dragon-Hatcher 5mo ago
  I've read the FAQ (https://github.com/aallan/vera/blob/main/FAQ.md https://github.com/aallan/vera/blob/main/FAQ.md) that provides the justification for this and it is, IMO, fairly weak. The main argument is that misleading names can confuse models. I have no problem believing this bit I'm not sure why we should assume code will have misleading names. In fact, the same document says that in tests they've had LLMs mix up the indices, which is exactly the problem I would foresee. It seems especially messy that the name for the same variable will change in different places in the code. The utility of De Bruijn indices is easy substitutability of expressions, which seems like totally the wrong thing to optimize for in a programming language. Edit: the more I think about it the more this seems like a really bad idea. Three more issues come to mind: 1) it becomes impossible to grep for a variable, which I know agents do all the time. 2) editing code at the top of the function, say introducing a new variable, can require editing all the code in the rest of the function, even if it was semantically unchanged! 3) they say it is less context for the LLM to track but now, instead of just having to know the name of one variable, you have to keep track of every other variable in the function
  - ArielTM 5mo ago
    [dead]
unignorant 5mo ago
This isn't my project, but I shared it here because it has a few important ideas I've been thinking about in my own work. Effect type systems in particular are a really good fit for LLMs because they allow you to reason very precisely about a program's capabilities before runtime (basically, using the type system for capability proofs). This helps you trust agent-created code (for example, you know it can't do IO), or, if the code does require certain capabilities, run it in a sandbox (e.g., mock network or filesystem). This kind of language design also provides a safer foundation for complex meta-systems of agents-that-create-agents, depending on how the runtime is implemented, though Vera may be somewhat limited in that particular respect. The major design decision I'm a little skeptical about is removing variable names; it would be interesting to see empirical data on that as it seems a bit unintuitive. I would expect almost the opposite, that variable names give LLMs some useful local semantics.
- still_grokking 5mo ago
  You're looking for Scala… ;-) https://news.ycombinator.com/item?id=47957121 https://news.ycombinator.com/item?id=47957121
danpalmer 5mo ago
> 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, LLMs are great. Java, similar. But writing Haskell, it's pretty bad, Erlang, not wonderful. You need much more of a mental model for those languages. For Vera, not having names removes key information that the model would have, and replaces it with mental modelling of the stack of arguments.
- smohare 5mo ago
  [dead]
- rapind 5mo ago
  > 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.
  - drob518 5mo ago
    But LLMs do Python quite well, so white space isn’t necessarily a problem.
    - mannykannot 5mo ago
      Yes - a point supported the Vera benchmark: https://github.com/aallan/vera-bench https://github.com/aallan/vera-bench
      - kgeist 5mo ago
        The benchmark is strange: single-run results (the author acknowledges it's unreliable) and uses older models like GPT-4o or Opus 4 (although the benchmark is from 2026).
2001zhaozhao 5mo ago
> 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.
- ycombinatornews 5mo ago
  Same here, reminds of JIRA’s field_17190 in MCP responses instead of description (and in similar excel-like systems) Good luck managing hallucinations on that context
- kgeist 5mo ago
  >The short answer is that variable names are one of the things that confuses LLMs rather than helps them. Unlike with humans, names undermine a model's efforts to keep track of state over larger scales. Models confuse similarly named variables in different parts of the codebase easily So I wonder, doesn't this apply to function names too, which the author keeps in? I've seen LLMs use wrong functions/classes as well. I think a proper harness, LSP and tests already solve everything Vera is trying to solve. They mostly cite research from 2021 before coding harnesses and agentic loops were a thing, back when they were basically trying to one-shot with relatively weak models (by modern standards)
  - imtringued 5mo ago
    The only way the author could have come up with that rationale is that he doesn't understand what a token is, what attention is and how coding agents work. Tokens combine multiple characters into a single vector. Attention computes similarity scores between vectors. This means you'd want each variable to be a single token so that the LLM can instantly know that two names refer to the same variable. If everything is numbered, the attention mechanism will attend every first parameter to every first parameter in every function. This means that the numbering scheme would have to be randomized instead of starting at zero. Coding agents are now capable of using tools, including text search, which means that having the ability to look for specific variable names is extremely helpful. By using numbering, the author of the language has now given himself the burden of relying entirely on LSPs rather than innate model properties that operate on the text level. So yeah, on a textual level, the language is designed for an era of LLMs that has been obsolete for a long time.
solomonb 5mo ago
I think Hindley Milner (for decidability) + Linear Types (for resource management) + Refinement Types (for lightly asserting invariants) + Delimited Continuation based Effects (for tracking effectful code) + Unison style Content Addressability (for corralling code changes, documentation, and tests) would make a really nice language for an LLM.
- still_grokking 5mo ago
  That's in large parts Scala. It doesn't have Hindley-Milner type inference, but it has very strong type inference. We will get linearity soon thanks to and as part of the Capybara[1] effort. Refinement types are already long a reality. The whole new effect tracking thing is based on delimited continuations. The Unison style content addressability comes up now and then, maybe it will become a reality at some point. It's though mostly not a language thing but more a build system thing. Scala is already great for for LLMs also for other reasons: https://arxiv.org/html/2510.11151v1 https://arxiv.org/html/2510.11151v1 [1] https://2025.workshop.scala-lang.org/details/scala-2025/6/System-Capybara-Capture-Tracking-for-Ownership-and-Borrowing https://2025.workshop.scala-lang.org/details/scala-2025/6/Sy...
  - solomonb 5mo ago
    AFAIK Scala's type system is not decidable. The point of Hindley Milner (and I really should have said System F without impredicative or higher rank types) was to get decidable polymorphism not type inference.
rtpg 5mo ago
The lack of naming seems to indicate a fundamental misunderstanding of how LLM coding agents are successful, and just makes me doubt anything about this project being useful and workable.
- svachalek 5mo ago
  Yeah it seems based on 2023 research which is ancient, back when we didn't have coding agents at all, and on some 1980s sci fi concepts of "how machines think" (beedeeboop) rather than the all too human coding agents we have. If I had to design one of these, I'd go for: 1. Token minimization (which may be circular, I'm sure tokens are selected for these models at least in part based on syntax of popular languages) 2. As many compile time checks as possible (good for humans, even better for machines with limited context) 3. Maximum locality. That is, a feature can largely be written in one file, rather than bits and pieces all over the codebase. Because of how context and attention work. This is the one I don't see much in commercially popular languages. It's more of a declarative thing, "configuration driven development".
  - Octoth0rpe 5mo ago
    > That is, a feature can largely be written in one file, rather than bits and pieces all over the codebase. This seems to be at odds with the goal of token minimization. Lots of small files that are narrowly scoped means less has to be loaded into context when making a change, right? Throwing out another idea: I wonder if we could see some kind of equivalent of c header files for more modern languages so that an llm just has to read the equivalent of a .h file to start using a library.
    - lesam 5mo ago
      I think AST aware code reading is criminally underused by agents - you don't need a header file if you can see a listing of all the functions in a library. Similarly, I don't read the whole file a function is in while editing it in an IDE, why should a coding agent get the whole file polluting its context by default?
DonHopkins 5mo ago
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.
- atgreen 5mo ago
  This is not my experience. I've been experimenting with something very similar to vera. However my language transpiles into multiple languages (Java, Typescript, Common Lisp, Rust, C++, Python, C# and Swift). The transpiler is written in the language itself (there's a separate bootstrap transpiler written in Common Lisp). But where I'm going is that Claude, at least, is extremely capable at writing decent code in my new language with barely any prompting; just minimal guidance on the language itself and no examples.
  - DonHopkins 5mo ago
    That's simply not true. That's just not the way LLMs work. LLMs are not magic. LLMs are stateless, they don't "remember" your bespoke programming language manual and examples between completion calls, so you have to repeatedly include all that with each and every completion call, which balloons the number of tokens used, reduces how much useful work you can do with the remaining tokens and attention, and is a costly waste of tokens and electricity and money. That isn't anywhere near as effective or efficient as using the LLM's pre-existing training on billions of lines of well known programming languages, manuals, tutorials, examples, code bases, stack overflow discussions, books, github repos, pr's, etc. What is your extraordinary evidence for your extraordinary claims? Have you empirically measured how well it works, or is it just vibes and handwaving?
sas41 5mo ago
I find the claims regarding LLMs and their mistake prone nature around variable names very confusing. It appears that me and creator have had vastly different experiences with LLMs and their capabilities with complex code bases and complicated business logic. My observations point to LLMs being much more successful when variables and methods have explicit, detailed names, it's the best way to keep them on track and minimize the chance of confusion, next closest thing being explicit comments and inline documentation. Poorly named and poorly documented things in a codebase only cause it to reason more on what it could be, often reaching a (wrong) conclusion, wasting tokens, wasting time. Perhaps this diversion in philosophy is due to fundamental differences in how we view the tool at hand. I do not trust the machine, as such I review it's output, and if the variables lacked names, that would be significantly harder. But if I had a "Jesus, take the wheel!" attitude, perhaps I'd care far less.
hybrid_study 5mo ago
I love the ## Why README section! Every repo should have one :-)
ConanRus 5mo ago
[dead]
firebot 5mo ago
Why not prolog or one of the other logic languages? It's really old, should be lots of good training data for it and the declarative nature would seem to be a great fit for llms.
- derdi 5mo ago
  Most Prolog code on the Web is complete garbage.
still_grokking 5mo ago
Why would anybody use a vibe-coded and vibe-desinged language which effectively does not exist yet instead of an established one with such features, like Scala? https://arxiv.org/html/2510.11151v1 https://arxiv.org/html/2510.11151v1
- davidw 5mo ago
  Also isn't it an advantage for LLM coding to use an existing language that has a lot of code that LLM's have already stol... I mean ingested?
  - fragmede 5mo ago
    Depends. A professor told me AI is really good at writing bad pandas code because it's seen a lot of bad pandas code, so starting from scratch isn't necessarily the worst thing.
  - still_grokking 5mo ago
    Exactly! Completely new languages without large amounts of reference material are terrible for LLMs.
rs545837 5mo ago
I agree 100% with this thinking approach, I've been working in this domain for quite a few months now. The right granularity for agents isn't files or lines, it's entities: functions, classes, methods. That's how both humans and agents actually think about code. We built sem(Ataraxy-Labs/sem) which extracts entities from 30+ languages via tree-sitter and builds a cross-file dependency graph, so building semantic version control and semantic diff. weave (same org) takes it further and does git merges at entity level. Matches functions by name, merges their bodies independently. The dependency graph also answers questions LLMs can't. I love the analysis based on ASTs.
offbyone42 5mo ago
I feel like this misses how LLMs work. Yes, you’re adding this layer of verification, but LLMs don’t think in ASTs or use formal logic. They are statistical predictors, just predicting what the next token will be. There is a reason they perform best with TS/PY and not Haskell. The difference in size of the code corpus for each language. The premise behind this seems to ignore all of that.
hahahacorn 5mo ago
I think the best language for LLMs is going to be as close to English as you can get with the compiler guarantees offered by Vera (or something similar). Seemingly opposing forces.
rickcarlino 5mo ago
Reminds me of http://cobra-language.com/ http://cobra-language.com/
signorovitch 5mo ago
> The evidence suggests the biggest problem models face isn't syntax So then why is the first mentioned and most obvious difference from other languages > There are no variable names. @Int.0 is the most recent Int binding LLMs are trained on code written by humans. They are most “familiar” with popular programming languages, have large datasets of examples and idioms to draw on. I don’t see the advantage of inventing a new language the machine must “learn” with syntax unlike anything it’s been trained on. Validation and testing are also already things we do with human written code, too.
- boxed 5mo ago
  Plus LLMs need semantics just like humans do. Maybe more. Removing variable names seems utter madness.
eranation 5mo ago
There are many problems we will need to address in the future. A programming language that is easy for machines to write but hard for humans to read isn’t one of them.
- Nevermark 5mo ago
  This isn't that different from circuit languages. Whittling everything down so the language is relatively 1-to-1 with the structure of the compute. With little or no extraneous decoration.
- MarceliusK 5mo ago
  [dead]
misja111 5mo ago
> Every function is a specification that the compiler can verify against its implementation. This has been tried so many times already. It works nice for functions that only do some arithmetic. But in any real life system that pushes data around over the network or to databases, most things will happen inside effects which leaves the compiler clueless as to whether the function implementation does what it's supposed to do or not. Don't get me wrong, I'm a big fan of using the compiler to improve productivity and I also believe strong typing leverages LLM power. But this kind of function specification is a dead end IMO.
eddythompson80 5mo ago
I’d ask for a refund on the tokens tbh
weddpros 5mo ago
It feels wrong to dump identifiers to save tokens: now they're devoid of semantics, and can't be grep'ed or mapped to concepts. CPUs are good with numbers, but LLMs are good with words.
tasuki 5mo ago
> Models struggle with maintaining invariants across a codebase, understanding the ripple effects of changes, and reasoning about state over time. I do, too!
anilgulecha 5mo ago
I think this is the wrong path in LLM and SWE optimizations: 1) Programming language training happens by volume, and the amount of JS/TS/python out there, and the rate it's growing at - is causing a training effects loop, which means for a few generations of models, these will be the best performing languages. Will be hard for a contender to spin up. 2) At some point, if we plateau on productivity - then efficiency improvements will happen, which will open a door for programming languages that maintains productivity, but is 10x cheaper on cost. 3) I think more immediate gains are at the cloud level. IMO, one of the reasons Google cloud is performing better(along with firebase) is much better overall CLI experience, leading to a pleasurable experience developing against it. This part of the market is ripe - whoever builds a most LLM friendly cloud has a shot of shooting up. Hence projects like exe.dev, and whatever cloudflare and vercel are trying. It would be good to have some shakeup in the cloud world. Anyway, this is where my thoughts are currently.
tasuki 5mo ago
> Traditional compilers produce diagnostics for humans: expected token '{'. Vera produces instructions for the model that wrote the code. Every error includes what went wrong, why, how to fix it with a concrete code example, and a spec reference. Is this a thing for the llms? As a human, I also prefer being told what went wrong and why and how to fix it, rather than `expected {`
kshri24 5mo ago
Providing a blackbox to the blackbox to reason. We are screwed
econ 5mo ago
I just renamed a dozen variables from short rather poor descriptions to good long ones and replaced array offsets with vars. The code changed from somewhat confusing code into easily readable. I'm usually not a fan of giantCamelCaseVarNames but if I have to map two dozen things to other things in my head my brain starts to lag and the limit of my context window makes me hallucinate. I do applaud the lang design effort as there are countless routes of accepting Jesus as your savior.
MarceliusK 5mo ago
The strongest idea here, IMO, is not the syntax but the feedback loop
Taikonerd 5mo ago
> The signature declares types, preconditions, postconditions, and effects. The compiler verifies the contract via SMT solver. This reminds me of Dafny: https://dafny.org/ https://dafny.org/ Actually, that's an interesting question: how good are LLMs at writing Dafny?
steffs 5mo ago
[dead]
peter_d_sherman 5mo ago
Related: Nanolang: A tiny experimental language designed to be targeted by coding LLMs https://news.ycombinator.com/item?id=46684958 https://news.ycombinator.com/item?id=46684958 https://github.com/jordanhubbard/nanolang https://github.com/jordanhubbard/nanolang SudoLang: A Powerful Pseudocode Programming Language for LLMs: https://medium.com/javascript-scene/sudolang-a-powerful-pseudocode-programming-language-for-llms-d64d42aa719b https://medium.com/javascript-scene/sudolang-a-powerful-pseu... Programming Without People: Designing a Language for LLMs: (ALaS (AI Language Specification)): https://dshills.medium.com/programming-without-people-designing-a-language-for-llms-2192618d2540 https://dshills.medium.com/programming-without-people-design... LMQL ("LMQL is a programming language for LLMs."): https://lmql.ai/ https://lmql.ai/ Which language is best for AI code generation? The answer might surprise you: https://revelry.co/insights/artificial-intelligence/which-language-is-best-for-ai-code-generation/ https://revelry.co/insights/artificial-intelligence/which-la...

111 points by unignorant 5mo ago

> Division by zero is not a runtime error — it is a type error. The compiler checks every call site to prove the divisor is non-zero. Elaborate a little here.

hgoel 5mo ago
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.
- hyperhello 5mo ago
  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?
  - hgoel 5mo ago
    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.
    - still_grokking 5mo ago
      Or it's just some AI brain fart… The whole things looks vibe-coded, and vibe-designed.
    - rdevilla 5mo ago
      > 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.
      - hyperhello 5mo ago
        Okay, int integer_division(int a, int b) { if (b!=0) return a/b; raise(SIGFPE); } Great.
        rdevilla 5mo ago
        You don't appear to understand the difference between runtime and static analysis/compile time, or term-level and type-level.
        hyperhello 5mo ago
        Great! Explain it to us while I read to my kid!
        cjbgkagh 5mo ago
        The ‘let me google that for you’ is set to be replaced with ‘let me ask ChatGPT for you’.
        rdevilla 5mo ago
        Don't get mad because you're too lazy to even ask the AI. You are first to be replaced in the workforce. Or maybe it's over your head and you should just stick to reading children's fiction after all. Want some colouring books too?
        hyperhello 5mo ago
        Yes! We can always use more books and toys here!
  - cjbgkagh 5mo ago
    Post type check analyzers can work with more than just the type information, you can really do whatever you want at this stage. The normal highly optimized type checker handles the bulk of the checking and the post type check analyzers can work on the residual. You wouldn’t type check a file that doesn’t parse, and you wouldn’t run the analyzers on code that doesn’t type check. 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).

ginko 5mo ago

Is there any evidence that using structural references rather than names allows large language models to generate better code? This bit just feels like obfuscation for obfustcation’s sake.

Dragon-Hatcher 5mo ago
I've read the FAQ (https://github.com/aallan/vera/blob/main/FAQ.md https://github.com/aallan/vera/blob/main/FAQ.md) that provides the justification for this and it is, IMO, fairly weak. The main argument is that misleading names can confuse models. I have no problem believing this bit I'm not sure why we should assume code will have misleading names. In fact, the same document says that in tests they've had LLMs mix up the indices, which is exactly the problem I would foresee. It seems especially messy that the name for the same variable will change in different places in the code. The utility of De Bruijn indices is easy substitutability of expressions, which seems like totally the wrong thing to optimize for in a programming language. Edit: the more I think about it the more this seems like a really bad idea. Three more issues come to mind: 1) it becomes impossible to grep for a variable, which I know agents do all the time. 2) editing code at the top of the function, say introducing a new variable, can require editing all the code in the rest of the function, even if it was semantically unchanged! 3) they say it is less context for the LLM to track but now, instead of just having to know the name of one variable, you have to keep track of every other variable in the function
- ArielTM 5mo ago
  [dead]

unignorant 5mo ago

This isn't my project, but I shared it here because it has a few important ideas I've been thinking about in my own work. Effect type systems in particular are a really good fit for LLMs because they allow you to reason very precisely about a program's capabilities before runtime (basically, using the type system for capability proofs). This helps you trust agent-created code (for example, you know it can't do IO), or, if the code does require certain capabilities, run it in a sandbox (e.g., mock network or filesystem). This kind of language design also provides a safer foundation for complex meta-systems of agents-that-create-agents, depending on how the runtime is implemented, though Vera may be somewhat limited in that particular respect. The major design decision I'm a little skeptical about is removing variable names; it would be interesting to see empirical data on that as it seems a bit unintuitive. I would expect almost the opposite, that variable names give LLMs some useful local semantics.

still_grokking 5mo ago
You're looking for Scala… ;-) https://news.ycombinator.com/item?id=47957121 https://news.ycombinator.com/item?id=47957121

danpalmer 5mo ago

> 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, LLMs are great. Java, similar. But writing Haskell, it's pretty bad, Erlang, not wonderful. You need much more of a mental model for those languages. For Vera, not having names removes key information that the model would have, and replaces it with mental modelling of the stack of arguments.

smohare 5mo ago
[dead]
rapind 5mo ago
> 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.
- drob518 5mo ago
  But LLMs do Python quite well, so white space isn’t necessarily a problem.
  - mannykannot 5mo ago
    Yes - a point supported the Vera benchmark: https://github.com/aallan/vera-bench https://github.com/aallan/vera-bench
    - kgeist 5mo ago
      The benchmark is strange: single-run results (the author acknowledges it's unreliable) and uses older models like GPT-4o or Opus 4 (although the benchmark is from 2026).

2001zhaozhao 5mo ago

> 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.

ycombinatornews 5mo ago
Same here, reminds of JIRA’s field_17190 in MCP responses instead of description (and in similar excel-like systems) Good luck managing hallucinations on that context
kgeist 5mo ago
>The short answer is that variable names are one of the things that confuses LLMs rather than helps them. Unlike with humans, names undermine a model's efforts to keep track of state over larger scales. Models confuse similarly named variables in different parts of the codebase easily So I wonder, doesn't this apply to function names too, which the author keeps in? I've seen LLMs use wrong functions/classes as well. I think a proper harness, LSP and tests already solve everything Vera is trying to solve. They mostly cite research from 2021 before coding harnesses and agentic loops were a thing, back when they were basically trying to one-shot with relatively weak models (by modern standards)
- imtringued 5mo ago
  The only way the author could have come up with that rationale is that he doesn't understand what a token is, what attention is and how coding agents work. Tokens combine multiple characters into a single vector. Attention computes similarity scores between vectors. This means you'd want each variable to be a single token so that the LLM can instantly know that two names refer to the same variable. If everything is numbered, the attention mechanism will attend every first parameter to every first parameter in every function. This means that the numbering scheme would have to be randomized instead of starting at zero. Coding agents are now capable of using tools, including text search, which means that having the ability to look for specific variable names is extremely helpful. By using numbering, the author of the language has now given himself the burden of relying entirely on LSPs rather than innate model properties that operate on the text level. So yeah, on a textual level, the language is designed for an era of LLMs that has been obsolete for a long time.

solomonb 5mo ago

I think Hindley Milner (for decidability) + Linear Types (for resource management) + Refinement Types (for lightly asserting invariants) + Delimited Continuation based Effects (for tracking effectful code) + Unison style Content Addressability (for corralling code changes, documentation, and tests) would make a really nice language for an LLM.

still_grokking 5mo ago
That's in large parts Scala. It doesn't have Hindley-Milner type inference, but it has very strong type inference. We will get linearity soon thanks to and as part of the Capybara[1] effort. Refinement types are already long a reality. The whole new effect tracking thing is based on delimited continuations. The Unison style content addressability comes up now and then, maybe it will become a reality at some point. It's though mostly not a language thing but more a build system thing. Scala is already great for for LLMs also for other reasons: https://arxiv.org/html/2510.11151v1 https://arxiv.org/html/2510.11151v1 [1] https://2025.workshop.scala-lang.org/details/scala-2025/6/System-Capybara-Capture-Tracking-for-Ownership-and-Borrowing https://2025.workshop.scala-lang.org/details/scala-2025/6/Sy...
- solomonb 5mo ago
  AFAIK Scala's type system is not decidable. The point of Hindley Milner (and I really should have said System F without impredicative or higher rank types) was to get decidable polymorphism not type inference.

rtpg 5mo ago

The lack of naming seems to indicate a fundamental misunderstanding of how LLM coding agents are successful, and just makes me doubt anything about this project being useful and workable.

svachalek 5mo ago
Yeah it seems based on 2023 research which is ancient, back when we didn't have coding agents at all, and on some 1980s sci fi concepts of "how machines think" (beedeeboop) rather than the all too human coding agents we have. If I had to design one of these, I'd go for: 1. Token minimization (which may be circular, I'm sure tokens are selected for these models at least in part based on syntax of popular languages) 2. As many compile time checks as possible (good for humans, even better for machines with limited context) 3. Maximum locality. That is, a feature can largely be written in one file, rather than bits and pieces all over the codebase. Because of how context and attention work. This is the one I don't see much in commercially popular languages. It's more of a declarative thing, "configuration driven development".
- Octoth0rpe 5mo ago
  > That is, a feature can largely be written in one file, rather than bits and pieces all over the codebase. This seems to be at odds with the goal of token minimization. Lots of small files that are narrowly scoped means less has to be loaded into context when making a change, right? Throwing out another idea: I wonder if we could see some kind of equivalent of c header files for more modern languages so that an llm just has to read the equivalent of a .h file to start using a library.
  - lesam 5mo ago
    I think AST aware code reading is criminally underused by agents - you don't need a header file if you can see a listing of all the functions in a library. Similarly, I don't read the whole file a function is in while editing it in an IDE, why should a coding agent get the whole file polluting its context by default?

DonHopkins 5mo ago

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.

atgreen 5mo ago
This is not my experience. I've been experimenting with something very similar to vera. However my language transpiles into multiple languages (Java, Typescript, Common Lisp, Rust, C++, Python, C# and Swift). The transpiler is written in the language itself (there's a separate bootstrap transpiler written in Common Lisp). But where I'm going is that Claude, at least, is extremely capable at writing decent code in my new language with barely any prompting; just minimal guidance on the language itself and no examples.
- DonHopkins 5mo ago
  That's simply not true. That's just not the way LLMs work. LLMs are not magic. LLMs are stateless, they don't "remember" your bespoke programming language manual and examples between completion calls, so you have to repeatedly include all that with each and every completion call, which balloons the number of tokens used, reduces how much useful work you can do with the remaining tokens and attention, and is a costly waste of tokens and electricity and money. That isn't anywhere near as effective or efficient as using the LLM's pre-existing training on billions of lines of well known programming languages, manuals, tutorials, examples, code bases, stack overflow discussions, books, github repos, pr's, etc. What is your extraordinary evidence for your extraordinary claims? Have you empirically measured how well it works, or is it just vibes and handwaving?

sas41 5mo ago

I find the claims regarding LLMs and their mistake prone nature around variable names very confusing. It appears that me and creator have had vastly different experiences with LLMs and their capabilities with complex code bases and complicated business logic. My observations point to LLMs being much more successful when variables and methods have explicit, detailed names, it's the best way to keep them on track and minimize the chance of confusion, next closest thing being explicit comments and inline documentation. Poorly named and poorly documented things in a codebase only cause it to reason more on what it could be, often reaching a (wrong) conclusion, wasting tokens, wasting time. Perhaps this diversion in philosophy is due to fundamental differences in how we view the tool at hand. I do not trust the machine, as such I review it's output, and if the variables lacked names, that would be significantly harder. But if I had a "Jesus, take the wheel!" attitude, perhaps I'd care far less.

hybrid_study 5mo ago

I love the ## Why README section! Every repo should have one :-)

ConanRus 5mo ago

[dead]

firebot 5mo ago

Why not prolog or one of the other logic languages? It's really old, should be lots of good training data for it and the declarative nature would seem to be a great fit for llms.

derdi 5mo ago
Most Prolog code on the Web is complete garbage.

still_grokking 5mo ago

Why would anybody use a vibe-coded and vibe-desinged language which effectively does not exist yet instead of an established one with such features, like Scala? https://arxiv.org/html/2510.11151v1 https://arxiv.org/html/2510.11151v1

davidw 5mo ago
Also isn't it an advantage for LLM coding to use an existing language that has a lot of code that LLM's have already stol... I mean ingested?
- fragmede 5mo ago
  Depends. A professor told me AI is really good at writing bad pandas code because it's seen a lot of bad pandas code, so starting from scratch isn't necessarily the worst thing.
- still_grokking 5mo ago
  Exactly! Completely new languages without large amounts of reference material are terrible for LLMs.

rs545837 5mo ago

I agree 100% with this thinking approach, I've been working in this domain for quite a few months now. The right granularity for agents isn't files or lines, it's entities: functions, classes, methods. That's how both humans and agents actually think about code. We built sem(Ataraxy-Labs/sem) which extracts entities from 30+ languages via tree-sitter and builds a cross-file dependency graph, so building semantic version control and semantic diff. weave (same org) takes it further and does git merges at entity level. Matches functions by name, merges their bodies independently. The dependency graph also answers questions LLMs can't. I love the analysis based on ASTs.

offbyone42 5mo ago

I feel like this misses how LLMs work. Yes, you’re adding this layer of verification, but LLMs don’t think in ASTs or use formal logic. They are statistical predictors, just predicting what the next token will be. There is a reason they perform best with TS/PY and not Haskell. The difference in size of the code corpus for each language. The premise behind this seems to ignore all of that.

hahahacorn 5mo ago

I think the best language for LLMs is going to be as close to English as you can get with the compiler guarantees offered by Vera (or something similar). Seemingly opposing forces.

rickcarlino 5mo ago

Reminds me of http://cobra-language.com/ http://cobra-language.com/

signorovitch 5mo ago

> The evidence suggests the biggest problem models face isn't syntax So then why is the first mentioned and most obvious difference from other languages > There are no variable names. @Int.0 is the most recent Int binding LLMs are trained on code written by humans. They are most “familiar” with popular programming languages, have large datasets of examples and idioms to draw on. I don’t see the advantage of inventing a new language the machine must “learn” with syntax unlike anything it’s been trained on. Validation and testing are also already things we do with human written code, too.

boxed 5mo ago
Plus LLMs need semantics just like humans do. Maybe more. Removing variable names seems utter madness.

eranation 5mo ago

There are many problems we will need to address in the future. A programming language that is easy for machines to write but hard for humans to read isn’t one of them.

Nevermark 5mo ago
This isn't that different from circuit languages. Whittling everything down so the language is relatively 1-to-1 with the structure of the compute. With little or no extraneous decoration.
MarceliusK 5mo ago
[dead]

misja111 5mo ago

> Every function is a specification that the compiler can verify against its implementation. This has been tried so many times already. It works nice for functions that only do some arithmetic. But in any real life system that pushes data around over the network or to databases, most things will happen inside effects which leaves the compiler clueless as to whether the function implementation does what it's supposed to do or not. Don't get me wrong, I'm a big fan of using the compiler to improve productivity and I also believe strong typing leverages LLM power. But this kind of function specification is a dead end IMO.

eddythompson80 5mo ago

I’d ask for a refund on the tokens tbh

weddpros 5mo ago

It feels wrong to dump identifiers to save tokens: now they're devoid of semantics, and can't be grep'ed or mapped to concepts. CPUs are good with numbers, but LLMs are good with words.

tasuki 5mo ago

> Models struggle with maintaining invariants across a codebase, understanding the ripple effects of changes, and reasoning about state over time. I do, too!

anilgulecha 5mo ago

I think this is the wrong path in LLM and SWE optimizations: 1) Programming language training happens by volume, and the amount of JS/TS/python out there, and the rate it's growing at - is causing a training effects loop, which means for a few generations of models, these will be the best performing languages. Will be hard for a contender to spin up. 2) At some point, if we plateau on productivity - then efficiency improvements will happen, which will open a door for programming languages that maintains productivity, but is 10x cheaper on cost. 3) I think more immediate gains are at the cloud level. IMO, one of the reasons Google cloud is performing better(along with firebase) is much better overall CLI experience, leading to a pleasurable experience developing against it. This part of the market is ripe - whoever builds a most LLM friendly cloud has a shot of shooting up. Hence projects like exe.dev, and whatever cloudflare and vercel are trying. It would be good to have some shakeup in the cloud world. Anyway, this is where my thoughts are currently.

tasuki 5mo ago

> Traditional compilers produce diagnostics for humans: expected token '{'. Vera produces instructions for the model that wrote the code. Every error includes what went wrong, why, how to fix it with a concrete code example, and a spec reference. Is this a thing for the llms? As a human, I also prefer being told what went wrong and why and how to fix it, rather than `expected {`

kshri24 5mo ago

Providing a blackbox to the blackbox to reason. We are screwed

econ 5mo ago

I just renamed a dozen variables from short rather poor descriptions to good long ones and replaced array offsets with vars. The code changed from somewhat confusing code into easily readable. I'm usually not a fan of giantCamelCaseVarNames but if I have to map two dozen things to other things in my head my brain starts to lag and the limit of my context window makes me hallucinate. I do applaud the lang design effort as there are countless routes of accepting Jesus as your savior.

MarceliusK 5mo ago

The strongest idea here, IMO, is not the syntax but the feedback loop

Taikonerd 5mo ago

> The signature declares types, preconditions, postconditions, and effects. The compiler verifies the contract via SMT solver. This reminds me of Dafny: https://dafny.org/ https://dafny.org/ Actually, that's an interesting question: how good are LLMs at writing Dafny?

steffs 5mo ago

[dead]

peter_d_sherman 5mo ago

Related: Nanolang: A tiny experimental language designed to be targeted by coding LLMs https://news.ycombinator.com/item?id=46684958 https://news.ycombinator.com/item?id=46684958 https://github.com/jordanhubbard/nanolang https://github.com/jordanhubbard/nanolang SudoLang: A Powerful Pseudocode Programming Language for LLMs: https://medium.com/javascript-scene/sudolang-a-powerful-pseudocode-programming-language-for-llms-d64d42aa719b https://medium.com/javascript-scene/sudolang-a-powerful-pseu... Programming Without People: Designing a Language for LLMs: (ALaS (AI Language Specification)): https://dshills.medium.com/programming-without-people-designing-a-language-for-llms-2192618d2540 https://dshills.medium.com/programming-without-people-design... LMQL ("LMQL is a programming language for LLMs."): https://lmql.ai/ https://lmql.ai/ Which language is best for AI code generation? The answer might surprise you: https://revelry.co/insights/artificial-intelligence/which-language-is-best-for-ai-code-generation/ https://revelry.co/insights/artificial-intelligence/which-la...