[em-bee]

exactly, i find the article a wierd take. i would have thougt that being able to catch errors at compile time is the assurance that the LLM generated code is actually decent.

so does this mean that the LLM writes code that is so good that the compiler does not find any more errors?

or is it due to the nature of haskell that makes it hard to write bad code to begin with?

or just that because the haskell compiler catches more errors there is less broken haskell code for the AI to train on?

and what does that mean for the switch to python? if the python compiler/interpreter doesn't catch as many errors do we even know that the code is good?

or is this more like the belief if the LLM can generate good haskell code, surely it can also generate good python?

what's the solution here? speeding up the haskell compiler? if that were easy, would it not already have happened?

personally i still don't trust LLM code generation. i didn't learn haskell yet, but what i hear about it makes me more likely to trust that LLMs can generate good haskell code than python.

i believe the future in LLM code generation is code that can be proven to be correct. proving code correct has been a research topic at some point.

[hunterpayne]

"proving code correct has been a research topic at some point."

It has been an area of active research for 40 years. But almost all the research returned the null result, meaning that the program proving didn't improve code quality (basically it didn't work). Yet somehow a group of programmers, usually fresh out of academia falls for program proving each generation. Strong types do really help but you need a good compiler which is sometimes lacking in the real work cough Scala cough. The problem with strong types and program proving is that the juice just isn't worth the squeeze meaning the extra time taken doesn't result in reduced debugging time or improved code quality. I don't think that changes with LLMs. It just exposes the flaws more quickly.

[frumplestlatz]

That's literally the opposite of reality; the research and adoption have consistently produced code of extremely high quality, at great cost.

The problem has always been:

- It's extremely labour-intensive, and even small changes to the code can require an enormous amount of new proof work.

- The skills required to formally verify software are very different from the skills required to write it, and the set of people capable of doing so is much smaller.

- Code has to be written with verification in mind, against a specification that expresses invariants that can actually be verified, and that is coherent enough that you can derive useful high-level properties of the system from it.

You needed two teams — verification and development. Verification would always be behind the development team, while also having to feed requirements and design changes back to the developers. Everything slowed to a crawl.

AI changes this. A coherent, verifiable, useful specification isn't easy to write — but it's far easier to write than the software itself, and AI can do most of that work: both drafting the spec and proving that it's consistent and that the high-level properties you actually care about follow from it.

More importantly, a high-level spec is far easier to read and reason about than the reams of code required to actually implement something. Which means:

- AI does the grunt work of writing and proving the spec; humans only have to carefully review that high-level artifact.

- AI writes code it must also prove conforms to the spec, so humans can be assured it's correct without babysitting the AI.

- Changes are driven top-down: evolve the spec first, then have the AI fix the implementation and re-prove conformance.

Our (very, very large) company is rapidly going all-in on formal verification across projects we never would have dreamed of verifying before; the velocity hit and the man-hour cost were only worth paying for truly critical infrastructure.

[doug_durham]

I’m sure in certain domains this makes sense. However, English is a poor language for doing reasoning in. More and more I’m relying on the code itself as the documentation. One of the superpowers of LLMs is reading code. and turning it into readable English. I don’t keep the English prose around. I delete it. In your example, I don’t see having two sets of artifacts. I see working with an LLM to generate a code base, which is the specification. You still need to have sets of requirements that list the invariants and other parameters. But the process becomes generating the code, and then having the LLM read the code to see if it meets the requirements and invariants.

[pmontra]

The issue with formal proofs is that we might end up with correct code that does the wrong thing. I mean, something that the market doesn't care about. At the same time a buggy set of PHP scripts does what people care about and captures the market. Think about 20+ years ago and you find a lot of examples.

[frumplestlatz]

Well, sure — and the issue with tests is we might end up with well-tested code that does the wrong thing.

[psd1]

https://xkcd.com/224/ lol

Zuckerberg became rich on php, which grinds my gears almost as much as the genocide thing.

In fairness, my peers at $corp used to ship while I was sad-Wojciech "no you can't create tech debt". The universe is cruel to people who care.

[lancepioch]

If that grinds your gears, then also take a look at Pieter Levels

[landdate]

php is a great language. there is a reason why the majority of the web runs on it.

[em-bee]

the reason is that php was accessible. it provided the bridge between pre coded serverside includes and writing your whole website in code, which you would have had to do with any other language. nowadays many things that php made easy can also be done with client side javascript.

i remember a conversation with a php core developer who conceded that one of the problems in the php community is a large number of inexperienced developers. it is similar problem that javascript faces today, but that, thanks to AI is going to affect more and more languages.

php itself is not a bad language, i use it too if it is appropriate, but it also has improved over the decades. so nowadays i am more likely to use php than i would have been a few decades ago.

[psd1]

There's a reason why littering is the most common crime - it doesn't require intelligence or planning, and whatever you are holding can instantly become trash.

[landdate]

if you were to ask people to rate crimes on morality i would presume littering would rank among the least immoral.

your point makes no sense. yes, if i had to pick one crime for someone to commit i might pick littering and many people think the same thing because littering is one of the most common crimes.

same thing is true for web development with php.

you absolute moron you don't even understand what you are saying just making random points that have a midwit cleverness, but when thought over by any respectable mind easily prove to be nonsense.

----

how could somebody like you think they deserve life enough to conjure up a breath let alone a word. It's a shame, and one you are too ignorant be aware of.

[em-bee]

that's a bit harsh.

[martl475]

Friend of mine said "Infuriatingly many people got rich with horribly bad software." (Sounds better in German)

[GregDavidson]

I've been successfully practicing programming with proof of correctness since the 1970s. The confusion I see with most people failing at this is that they're trying to write code first and then prove it correct. The idea promoted by Dijkstra, Hoare, et al is to write the code and the proof together, with each of these aspects of the task supporting the other. The result is (in my experience) a better program developed as quickly (even when not counting on vastly decreased debugging time) as pure coding. Similarly with strong lexical typing: One does not try to create a typing model for a hunk of arbitrary code. Instead, one develops the type model along with the code, with each of those aspects supporting the other. Putting it all together: Coding, Typing (and other Constraining) and Proving are done together, with each of these activities supporting the others. It does take time to learn such a methodology. And it takes extra understanding to maintain types, constraints and proofs as the program evolves, i.e. "maintenance".

[hollerith]

Can you show us a proof of correctness you've written?

[em-bee]

what i expect to change with LLMs is the benefit you get from automated testing. which is really what LLMs need. tools that tell you something is wrong may not speed up a human developer, but they will allow LLMs to make corrections by itself until the warnings go away. so while it may not be worth it to a human developer, it may well be worth it for an LLM.

[tonyarkles]

> what's the solution here? speeding up the haskell compiler? if that were easy, would it not already have happened?

I suspect you’ve nailed the answer: it’s probably not easy, although it’s also possible that it just hasn’t ever had a lot of attention paid to it because it’s been generally fast enough for their user base?

[antonvs]

Part of the issue is probably that Haskell build performance is perfectly fine for local development, even on rather large systems.

But in commercial production environments, CI pipelines tend to want to build everything from scratch every time, and that slows everything down. Rust has the same issue. Both languages, by default, compile all their dependencies from source, rather than obtaining precompiled artifacts from a repo the way some languages (like Java) do. And their compilers are slower than e.g. Go's. As the article mentions, various kinds of caching can help with that, but that's extra stuff you have to manage and deal with.

I'm not sure this is a bad thing, though. Haskell co-creator Simon Peyton-Jones coined the unofficial Haskell motto, "avoid success at all costs". I tend to agree with that. It would be difficult for Haskell to maintain its conceptual edge if it were a mainstream commercial language.

[cwillu]

The thing I hate about rust is that compiling a small app immediately creates 100gb of junk, and that junk doesn't live in the responsible project's folder, and that junk doesn't get cleaned up by anything.

[pdimitar]

You're exaggerating quite a lot. Biggest I've seen the cargo directory after 3 months of active Rust development was ~17GB.

You can also limit it with an env var. I have capped mine at 10GB.

[kstrauser]

I’m at 227GB as I write this.

[pdimitar]

Super curious then, and I stand corrected.

You can put the `cargo clean gc` command on a daily/weekly schedule then, or configure the `gc` option in your Cargo config. Or set `CARGO_UNSTABLE_GC=true` in your shell init. Or all of the above.

[valcron1000]

Had no nuke the `target` folder a couple of weeks ago, +400 GB ...

[capitainenemo]

Many rust nightly versions + no clean / sweep / clean-all?