News for hackers. Stuff that matters.
Re:Kotlin creator's new language: a formal way to talk to LL... by stephbook on Thursday March 12, 2026 @04:44PM (#47356817)
> It’s one of those things that crackpots keep trying to do, no matter how much you tell them it could never work. If the spec defines precisely what a program will do, with enough detail that it can be used to generate the program itself, this just begs the question: how do you write the spec? Such a complete spec is just as hard to write as the underlying computer program, because just as many details have to be answered by spec writer as the programmer.

Joel Spolsky, stackoverflow.com founder, Talk at Yale: Part 1 of 3 https://www.joelonsoftware.com/2007/12/03/talk-at-yale-part-...

Re:Kotlin creator's new language: a formal way to talk to LL... by sethev on Thursday March 12, 2026 @04:56PM (#47356973)
Program generation from a spec meant something vastly different in 2007 than it does now. People can and are generating programs from underspecified prompts. Trying to be systematic about how prompts work is a worthwhile area to explore.
Re:Kotlin creator's new language: a formal way to talk to LL... by ModernMech on Thursday March 12, 2026 @11:58PM (#47360534)
Isn't that how it always goes? First its just the crackpots. Then it's a fringe. Soon it's the way things have always been done.
Re:Kotlin creator's new language: a formal way to talk to LL... by redwolf2 on Friday March 13, 2026 @07:23AM (#47362938)
Might look like it, might also just be survivorship bias. Alot of crackpot ideas hit the wall instead of beeing a success. We only notice the successors and might think of them as the default, not the exception.
Re:Kotlin creator's new language: a formal way to talk to LL... by ModernMech on Saturday March 14, 2026 @07:34AM (#47375605)
I was commenting from that perspective, basically any thing we consider today to be “the way it’s done” was once something only crazy people did. I think maybe it was pg who said something like if you’re only working on safe things you’ll never have a breakthrough because if breakthroughs came from safe ideas then there would be more of them. I’m not saying every crazy idea changes the world but if you want to change the world you need a crazy idea.
Re:Kotlin creator's new language: a formal way to talk to LL... by prohobo on Friday March 13, 2026 @03:31AM (#47361599)
So is that what CodeSpeak does? It formalizes the vocab/structure of prompts?
Re:Kotlin creator's new language: a formal way to talk to LL... by akvadrako on Friday March 13, 2026 @04:39AM (#47361961)
I don't see how it's different. You could always describe what you want to a team lead or consultant and pay them to build it.

That's still the best way to turn a spec into a program and comes with all the downsides it entails.

Re:Kotlin creator's new language: a formal way to talk to LL... by sethev on Friday March 13, 2026 @09:06AM (#47363945)
Sure, but Joel isn't saying that's impossible or that people who do that are crackpots. In fact, he was an advocate of writing specs ahead of time [1] - for people.

At the time "generating a program from a spec" was an idea floating around that you could come up with a "spec language" that was easier than regular programming languages but somehow still had the same power and could be compiled directly into a program. That's the crackpot idea that Joel is referencing - but that's not what a spec language used with an LLM is doing.

[1]: https://www.joelonsoftware.com/2000/10/02/painless-functiona...

Re:Kotlin creator's new language: a formal way to talk to LL... by jason_oster on Friday March 13, 2026 @02:03PM (#47367582)
This is an excellent observation and puts into words something I have barely scratched the surface of. Along with specifications, formal verification is another domain that received the "just automate it" treatment in the before times.

And because formal verification with LLMs is an active area of open research, I have some hope that the old idea of automated formal verification is starting to take shape. There is a lot to talk about here, but I'll leave a link to the 1968 NATO Software Engineering Conference [1] for those who are interested in where these thoughts originated. It goes deeply into the subject of "specification languages" and other related concepts. My understanding is that the historical split between computing science and software engineering has its roots in this 1968 conference.

[1]: http://homepages.cs.ncl.ac.uk/brian.randell/NATO/nato1968.PD...

Re:Kotlin creator's new language: a formal way to talk to LL... by jasfi on Saturday March 14, 2026 @01:42AM (#47373705)
I've built an AI compiler that has my take on this: https://github.com/jfilby/intentcode
Re:Kotlin creator's new language: a formal way to talk to LL... by stephbook on Saturday March 14, 2026 @03:09AM (#47374106)
Why don't you simply point your agent to your Jira tickets? It's easier than paying another third party for their magic LLM incantation loop.
Re:Kotlin creator's new language: a formal way to talk to LL... by slcjordan on Thursday March 12, 2026 @05:08PM (#47357135)
It actually makes sense that code is becoming amorphous and we will no longer scale in terms of building out new features (which has become cheap), but by defining stricter and stricter behavior constraints and structural invariants.
Re:Kotlin creator's new language: a formal way to talk to LL... by embedding-shape on Thursday March 12, 2026 @05:48PM (#47357669)
Yeah, "what you're able to build" is no longer one of the most important things, "what you won't build" just became a lot more important.
Re:Kotlin creator's new language: a formal way to talk to LL... by CamperBob2 on Thursday March 12, 2026 @04:46PM (#47356852)
What he misses is that it's much easier to change the spec than the code. And if the cost of regenerating the code is low enough, then the code is not worth talking about.
Re:Kotlin creator's new language: a formal way to talk to LL... by mwarkentin on Thursday March 12, 2026 @04:53PM (#47356935)
Is it? If the spec is as detailed as the code would be? If you make a change to one part of the spec do you now have inconsistencies that the LLM is going to have to resolve in some way? Are we going to have a compiler, or type checker type tools for the spec to catch these errors sooner?
Re:Kotlin creator's new language: a formal way to talk to LL... by CamperBob2 on Thursday March 12, 2026 @05:25PM (#47357353)
It IS a compiler. You might as well ask if the machine-language output of a C compiler is as detailed as the C code was.

To anticipate your objection: you can get over determinism now, or you can get over it later. You will get over it, though, if you intend to stay in this business.

Re:Kotlin creator's new language: a formal way to talk to LL... by discreteevent on Thursday March 12, 2026 @06:13PM (#47357990)
> It IS a compiler.

What are you talking about? If an LLM is a compiler, then I'm a compiler. Are we going to redefine the meaning of words in order not to upset the LLM makers?

Re:Kotlin creator's new language: a formal way to talk to LL... by reverius42 on Friday March 13, 2026 @02:50AM (#47361393)
Originally, the word "computer" referred to a human being. See https://en.wikipedia.org/wiki/Computer_(occupation)

Over time, when digital computers became commonplace, the computing moved from the person to the machine. At this time, arguably the humans doing the programming of the machine were doing the work we now ask of a "compiler".

So yes, an LLM can be a compiler in some sense (from a high level abstract language into a programming language), and you too can be a compiler! But currently it's probably a good use of the LLM's time and probably not a good use of yours.

Re:Kotlin creator's new language: a formal way to talk to LL... by jason_oster on Friday March 13, 2026 @03:25PM (#47368580)
I don't know, having done a lot of completely pointless time-wasting staring at hex dumps and assembly language in my youth was a pretty darned good lesson. I say it's a worthwhile hobby to be a compiler.

But your point stands. There is a period beyond which doing more than learning the fundamentals just becomes toil.

Re:Kotlin creator's new language: a formal way to talk to LL... by James_K on Thursday March 12, 2026 @05:45PM (#47357641)

  import Mathlib
  def Goldbach := ∀ x : ℕ, Even x → x > 2 → ∃ (y z: ℕ), Nat.Prime y ∧ Nat.Prime z ∧ x = y + z
A short specification for the proof of the Goldbach conjecture in Lean. Much harder to implement though. Implementation details are always hidden by the interface, which makes it easier to specify than produce. The Curry-Howard correspondence means that Joel's position here is that any question is as hard to ask as answer, and any statement as hard to formulate as it is to prove, which is really just saying that all describable statements are true.
Re:Kotlin creator's new language: a formal way to talk to LL... by xigoi on Friday March 13, 2026 @03:47AM (#47361672)
This argument is based on the notion of proof irrelevance – if a theorem is true, any proof is as good as any other. This is not the case for computer programs – two programs that implement the same specification may be very different in terms of performance, size, UI/UX, code maintainability, etc.
Re:Kotlin creator's new language: a formal way to talk to LL... by James_K on Friday March 13, 2026 @11:19AM (#47365665)
Performance and size can easily be added to any specification, maintainability is not a problem if you never have to maintain it, UI/UX are design issues not code issues. If you specify a UI, it will have the UX you want. We can already do UI creation with visual editors.
Re:Kotlin creator's new language: a formal way to talk to LL... by antonvs on Friday March 13, 2026 @04:21AM (#47361853)

    theorem goldbach : Goldbach := *message truncated*
Re:Kotlin creator's new language: a formal way to talk to LL... by TiredOfLife on Thursday March 12, 2026 @09:07PM (#47359509)
> The horse is here to stay, but the automobile is only a novelty — a fad.

Advice given to Henry Ford’s lawyer, Horace Rackam, by an unnamed president of Michigan Savings Bank in 1903.

Re:Kotlin creator's new language: a formal way to talk to LL... by bitwize on Thursday March 12, 2026 @10:37PM (#47360065)
People literally specifying software into existence in 2026 gives this quote a vibe of "aerodynamically speaking, bumblebees cannot fly".
Re:Kotlin creator's new language: a formal way to talk to LL... by xigoi on Friday March 13, 2026 @03:50AM (#47361689)
You can only specify software into existence if your idea of what you want it to look like is as vague as your specification. Sometimes this is the case, sometimes not.
Re:Kotlin creator's new language: a formal way to talk to LL... by ekropotin on Friday March 13, 2026 @01:20AM (#47360992)
I’m actually start seeking at work how people are writing skills in a very procedural manner. Something like:

First, collect the following information from user: …. Second, send http request to the following endpoint with the certain payload…. If server returned error - report back to user.

It makes me crack every time I see that kind of stuff. Why on Earth you won’t just write a script for that purpose? 10x faster, zero tokens burned, 100% deterministic.

Re:Kotlin creator's new language: a formal way to talk to LL... by KingMob on Friday March 13, 2026 @03:22AM (#47361558)
> Why on Earth you won’t just write a script for that purpose?

- Because your bash-fu may not be good enough

- Because parts of the process may not be amenable to scripting, especially if they require LLMs

- Because the inputs to some steps are fuzzy enough that only an LLM can handle them

- etc...

That being said, yes, anything amenable to being turned into scripts should be.

Re:Kotlin creator's new language: a formal way to talk to LL... by pjmlp on Friday March 13, 2026 @04:38AM (#47361959)
Because then you cannot meet the KPIs of using AI tools on the job. /s
Re:Kotlin creator's new language: a formal way to talk to LL... by patcon on Friday March 13, 2026 @10:36AM (#47365085)
Non-obvious solution Joel wasn't thinking of pre-AI age: you obviously just invent a mind crystal to interpret the spec during the build process ;)