Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Vera: a programming language designed for machines to write

github.com

Post reply on HN
Print view View original

81–90 of 105 posts

Re: Vera: a programming language designed for machines to write

#81

Post by mkl »

danpalmer wrote: post #5

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

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

I don't think that follows. It could just be that there is way more Go and Java code to train on than Haskell and Erlang. Haskell's terseness and symbol-named operators probably don't help either.

Re: Vera: a programming language designed for machines to write

#83

Post by derdi »

hyperhello wrote: post #46
rdevilla wrote: post #45

Earlier quoted context omitted.

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

Okay, int integer_division(int a, int b) { if (b!=0) return a/b; raise(SIGFPE); } Great.

No. In this type of language, the typical division function does not check against zero. It has a precondition that requires the caller to ensure that the divisor is not zero. If the data the caller has is completely arbitrary, then yes, the caller must use an if statement or similar. If the caller knows something about its data and can be sure that the divisor is not zero, then it doesn't need to use an if statement. But it might need to convince the proof checker that it knows what it's doing.

Re: Vera: a programming language designed for machines to write

#84

Post by anilgulecha »

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.

Re: Vera: a programming language designed for machines to write

#85

Post by tasuki »

> 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 {`

Re: Vera: a programming language designed for machines to write

#86

Post by tasuki »

ecthiender wrote: post #77
danpalmer wrote: post #5

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

Hmm, interesting. Are you speaking from experience for Haskell? I'm a Haskell developer since 2017, and have been using LLMs to write code (including Haskell) since 2024. In my experience, LLMs perform much better generating Haskell/Rust code over Python/Javascript.

Same experience. Being able to iterate on compile errors is helpful.

Re: Vera: a programming language designed for machines to write

#88

Post by kgeist »

mannykannot wrote: post #51
drob518 wrote: post #49

Earlier quoted context omitted.

But LLMs do Python quite well, so white space isn’t necessarily a problem.

Yes - a point supported the Vera benchmark: https://github.com/aallan/vera-bench

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

Re: Vera: a programming language designed for machines to write

#89

Post by classified »

danpalmer wrote: post #5

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

If it's incomprehensible to humans, it must be perfect for LLMs. Never mind the training.
Post reply on HN