Rendered at 04:26:17 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
andai 6 hours ago [-]
> External/world effects are visible in function signatures
Brilliant. I think Jai has something like that? Each function declares what it's going to touch (both read/write) globally, and I think you can specify that per block even.
I haven't used Jai (I think it's not out yet) but I remember the author talking about this and it sounded like a great idea.
It's related to the idea of pure functions being easy to reason about. Right now most languages don't even have a concept of pure functions, but the ones that do, just have two categories. When a function is messing with global state you do actually want to know what it's doing.
I think that can be statically computed (and displayed as IDE annotations or whatever) but specifying it explicitly sounds like a good practice either way.
I like that you're including other side effects (e.g. network) there too though, that's pretty cool!
Another thing I'm really interested in is proofs. Not necessarily total proofs (though we seem to be moving in that direction, at least for subsets of the codebase), but just normalizing rudimentary pre and post conditions checks.
I was thinking of setting it up so code can't even compile in release mode if those are missing. (Not every function would need them, but you at least want to state their absence explicitly.)
I was also thinking of setting up strictness levels per function, using hashing or something, so if a function is modified, you'd have to go through a process of double checking it again. And then functions labeled e.g. level 7 strict couldn't call ones with a lower proven strictness level, and so on. I'm told that I've basically been reinventing Ada from first principles so I should probably go and take a look at that...
Wait, your thing is doing hashing too... Woah. (I think that comes from proofs land or something?)
jbwinters 3 hours ago [-]
Thanks for the pointer to Jai! I will check it out.
Yes, Jacquard uses content-addressed definitions and it should be possible to set up a process for 'review again if this changes' on top of it. Warp, the testing framework, already uses this to avoid rerunning pure tests when neither the definition or dependencies have changed.
Jacquard does not currently implement proof or strictness levels, but binding those to a definition’s content identity is interesting and definitely worth exploring.
What are you building that people keep comparing to Ada?
andai 53 minutes ago [-]
Haven't built anything yet as far as language / tooling goes, but my experiences with poorly designed languages and tooling have basically made me paranoid as far as "what touches this variable", "what does this function actually do", ended up arriving in Rust / Haskell-ish territory just by recoiling from the pain of PHP/WordPress, where everything is global, mutable, dynamic and designed to make you go completely insane.
(In a nutshell: the more dynamic a programming language is, the more impossible it becomes to reason about what the program is doing. That's fine for throwaway scripts and game jams (#pragma JamMode), but the "the program is probably seriously wrong" should be explicitly opt-in, not the default ...)
So my current approach is everything should be as local as possible, as immutable as possible, etc. Basically Rust except I'm not a fan of low level programming. (I basically want Rust With GC (C# memory model), which sends Rust folks into paroxysms!)
I want it stricter than Rust in many respects, but also less annoying. (Better ergonomics and higher level, with a low level escape hatch when needed.)
Swift is apparently close to that, and might deserve another look.
I've also been obsessed with formal verification and proofs except, today I had a very revealing experience. I had an LLM incorrectly implement a major feature, and "verify" it with several thousand lines of tests. It was, as implemented, backwards, and also completely pointless — but all tests came back green!
I laughed when I realized, if it had been done in Rust, and with a layer of formal verification... well all the proofs (of the stupid and wrong and backwards thing) would have come back green too... It would have mathematically proven that the incorrect thing was correct...
jbwinters 37 minutes ago [-]
Ah, that’s a tough one. My hope is that Jacquard, or some similar language, can make intent explicit through readable, high-level constructs, giving both the human reviewer and the model a clearer target while the details are filled in. But it still can’t tell us whether the original intent was right.
Coincidentally, you reminded me of one of my favorite Charles Babbage quotes:
> “On two occasions I have been asked, ‘Pray, Mr. Babbage, if you put into the machine wrong figures, will the right answers come out?’ I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question.”
I suppose catching that kind of mistake is how humans prove to our future AI overlords that we should be kept around.
42 minutes ago [-]
lolinder 2 hours ago [-]
Not just effects, multi-shot effects:
> Algebraic effects with deep, multi-shot handlers. A handler can resume a computation zero, one, or many times, which is what makes exhaustive search and exact inference ordinary library code.
I love me some algebraic effects, but this sets off alarm bells for me.
Multi-shot effects are neat and powerful but are incredibly difficult to reason about for humans, and given that there are few languages that have implemented them (and they're so niche with very little training data) I'm skeptical that LLMs are sufficiently better at them to make up the gap.
One-shot effects are a cross between `throw` and a function call. Multi-shot are full-on delimited continuations and come with all the complexity that entails.
ch4s3 57 minutes ago [-]
> Multi-shot effects are neat and powerful but are incredibly difficult to reason about for humans
I had a very similar thought and ended up building a capability system[1] in my language to capture side effects.
AST hashing & effects are both used in Unison, if you want to check that out. I don't know that they have any proof-land stuff, though.
keithba 20 minutes ago [-]
Very cool!
I’ve been very fascinated by the concept of a programming language designed for LLMs, both to that advantage of their strengths and to try and minimize their weaknesses.
(Note: main has a version that was an ugly syntax, the branch in the link was for a prettier attempt)
wren6991 7 hours ago [-]
Given how poorly LLMs do with writing prompts for LLMs, I'm not sure I'd trust their judgement in designing a language for LLMs.
> and the runtime requires explicit permission to touch the filesystem, network, etc
This feels like more of an OS problem (or library problem) than a language problem.
> Run one program against many worlds. The same code can run against the real network, a scripted fake, a recording of last week's traffic, or a probability model of how servers usually behave
How is the "world" model different from plain dependency injection?
vineyardmike 6 hours ago [-]
> How is the "world" model different from plain dependency injection?
In addition to what the other comment said, this "world" model is great for hermetic testing of complex code, LLM written or not. We've seen existing projects that intercept the OS level syscall for testing, replayability, etc. Building it into the language runtime, hopefully with better ergonomics from the start than a syscall, would be a welcome addition broadly.
lolinder 14 minutes ago [-]
Dependency injection provides the same hermetic-testing capability, so that's not really an answer to OP's question. Effect-as-world-model is, in this specific way, just a special argument slot that only accepts dependency-injected functions.
What effects provide beyond DI is entirely in their ability to abort (resume zero times) or (in the case of multi-shot effects) resume multiple times. An effect that resumes exactly once is structurally the same as a dependency injected lambda.
embedding-shape 5 hours ago [-]
> Given how poorly LLMs do with writing prompts for LLMs, I'm not sure I'd trust their judgement in designing a language for LLMs.
Yeah agree, what I really want to see now, is a programming language for LLMs, designed by a human (although code could still be LLM-made I suppose), and see how both of them fare in various scenarios.
But basically world is a bit more narrow, that moment where your code touches the outside world (logging, http, etc), you can swap that. It's sorta like DI but deliberately narrower, only the moments where code touches the outside world are swappable.. With DI in theory you can replace anything, which has its benefits, but at least personally I am not a big fan of mocks, except when they touch the outside world. So that's what's replaceable.
skybrian 60 minutes ago [-]
These effect systems seem nice enough when all your I/O is going through a narrow interface, but I'm wondering what happens when you have a very large API surface, like everything available to a web page running in a browser?
Fricking training distribution/same-y ness coming for us all… cool project though.
orbital-decay 4 hours ago [-]
The distribution is actually pretty diverse, but this diversity is constrained by mode collapse.
jbwinters 3 hours ago [-]
It's a good name regardless! Don't stop on my account.
parpfish 2 hours ago [-]
a feature that i thought would be good for llm-centric languages would be making something like python's doctest prominent where you put simple little unit tests in the docstring of the function rather than in some testing module someplace else.
it would make it easy for humans to easily stub out tests with a docstring description and the tests that would guarantee certain behaviors. for the machine, it'd make it easy to add in new tests because the function+tests are in the same context window
troupo 1 hours ago [-]
> for the machine, it'd make it easy to add in new tests because the function+tests are in the same context window
Given how many useless unit tests Codex just loves to write, no, thank you.
Thankfully, its training data completely misses this. So at least for now it completely ignores doctests (at least in Elixir).
phildenhoff 5 hours ago [-]
Very cool -- I often thought that Unisons caching approach should be adopted more widely. Look forward to poking at it later!
sajithdilshan 7 hours ago [-]
I love how people create so many new things with AI, but to think how much tokens, and in turn money we all have collectively burned for these side projects is crazy.
staticshock 5 hours ago [-]
We only come to understand idea quality via evolutionary fitness tests, which means we have to MAKE things in order to find out if they're any good. Everything you make is gonna do hill-climbing in a [potentially unstable] environment in search of an ecological niche. This is true of species a la Darwin, but it's also true of products & ideas.
Anything we make gets to participate in this evolutionary process, even if it sounded dumb at the outset. In fact, doing dumb things is how we get "unstuck" from outdated ways of thinking.
unreal6 7 hours ago [-]
As long as token costs are being subsidized, I don't mind that this is the result of the consumer surplus.
jpadkins 6 hours ago [-]
it pales in comparison to all the brain cells burned chasing dumb ideas. Don't sweat it, and keep burning tokens in an effort to discover something great.
sinuhe69 3 hours ago [-]
Not just money. A lot of CO2 was dumped into our atmosphere and tons of clean water were evaporated as well.
skeledrew 2 hours ago [-]
Streaming videos and playing heavy online games has a similar effect. Which do you think should be preferable: watching ~3 hours of video streaming, or generating a respectably-sized project that perfectly scratches an itch?
applfanboysbgon 2 hours ago [-]
I don't really have a dog in this race, but "3 hours of streaming" is several orders of magnitude off using a frontier model to write a project like this. Like, 3000 hours of streaming would be closer. Then you're talking about one person consuming the resources for a useless project they'll abandon after a week vs. the resources consumed providing years of entertainment.
skeledrew 38 minutes ago [-]
How did you get 3000? That's a wildly inaccurate and out-of-this-world figure. I did some preliminary research recently that I'm not fully recalling (would have to look for it), but I had a baseline of something like 9 minutes of streaming video using the equivalent resource (electricity, etc) of just over 5 average prompts. So 3 hours of streaming video is a bit over 1000 prompts.
I can get an OK tool that still goes a good distance in scratching an itch in say ~3-8 prompts, so with 1000 I'm looking at a small app. With 100000... I'm finding it a bit hard to imagine TBH; somewhere in the region of the Bun port to Rust[0] is my likely-off-base-but-not-as-bad-as-yours guess. Heck just consider that there are devs out there running systems with local models that are probably more than half the size of a frontier model, and how that 3000-hours-equivalent cost would've been eating into their pockets in the form of electricity bills.
The obvious problem with any new AI-centric programming language (I think this is the third I’ve seen at this point) is that any LLM you try to use with it will be starting from zero - it has nothing to copy from and very little documentation available to find on its own, if it’s even capable of doing web searches. Java or C++ or whatever may be “worse” by some standards for LLMs (or humans) to work with, but all LLMs in common use have already been trained on decades of existing code which it can crib from.
jbwinters 1 hours ago [-]
This is definitely true. The language is intentionally small enough to fit into a single SKILL.md file, for what it's worth:
Agents I've tested with have had been able to pick up the language from that, at least to the extent that I've been able to test so far.
ch4s3 55 minutes ago [-]
> very little documentation available to find on its own
Building something like haskel's hoogle seems like a smart approach to this problem.
foxes 4 hours ago [-]
An llm doesnt 'prefer' to use anything.
Whats different to the effects system just being a type system?
Isnt a function that opens a particular file still just a type? Perhaps dependent?
Reminds me of mercury which has determinism of the function like type signatures.
jbwinters 2 hours ago [-]
You're right, an LLM doesn't have preferences. As shorthand, I thought it a useful concept though, as they do have particular ways of writing that can be tuned for.
The effect system here is part of a type system (technically a type-and-effect system). Where a value type typically describes what value a computation returns, an effect describes which operations it can perform during evaluation.
The difference is that effects propagate through the call graph, so lower-level code cannot access disallowed resources without that authority appearing higher up. At runtime, world effects also require an explicit grant. In a typical value type system, lower-level code can introduce side effects without them appearing in the caller’s type.
12 hours ago [-]
10 hours ago [-]
erelong 7 hours ago [-]
"Esperanto for Clankers"
Merkur 5 hours ago [-]
Yea, LLM remove the burden of typing - so if token cost don’t explode the new high-level languages will be above the current - and the new low-level language will maybe just weights…
lyu07282 46 minutes ago [-]
Like to believe we will one day use a low level language that is non-deterministic to build everything on top off seems to me in violation of such fundamental laws of information theory it's on the level of a belief in telekinesis.
Brilliant. I think Jai has something like that? Each function declares what it's going to touch (both read/write) globally, and I think you can specify that per block even.
I haven't used Jai (I think it's not out yet) but I remember the author talking about this and it sounded like a great idea.
It's related to the idea of pure functions being easy to reason about. Right now most languages don't even have a concept of pure functions, but the ones that do, just have two categories. When a function is messing with global state you do actually want to know what it's doing.
I think that can be statically computed (and displayed as IDE annotations or whatever) but specifying it explicitly sounds like a good practice either way.
I like that you're including other side effects (e.g. network) there too though, that's pretty cool!
Another thing I'm really interested in is proofs. Not necessarily total proofs (though we seem to be moving in that direction, at least for subsets of the codebase), but just normalizing rudimentary pre and post conditions checks.
I was thinking of setting it up so code can't even compile in release mode if those are missing. (Not every function would need them, but you at least want to state their absence explicitly.)
I was also thinking of setting up strictness levels per function, using hashing or something, so if a function is modified, you'd have to go through a process of double checking it again. And then functions labeled e.g. level 7 strict couldn't call ones with a lower proven strictness level, and so on. I'm told that I've basically been reinventing Ada from first principles so I should probably go and take a look at that...
Wait, your thing is doing hashing too... Woah. (I think that comes from proofs land or something?)
Yes, Jacquard uses content-addressed definitions and it should be possible to set up a process for 'review again if this changes' on top of it. Warp, the testing framework, already uses this to avoid rerunning pure tests when neither the definition or dependencies have changed.
Jacquard does not currently implement proof or strictness levels, but binding those to a definition’s content identity is interesting and definitely worth exploring.
What are you building that people keep comparing to Ada?
(In a nutshell: the more dynamic a programming language is, the more impossible it becomes to reason about what the program is doing. That's fine for throwaway scripts and game jams (#pragma JamMode), but the "the program is probably seriously wrong" should be explicitly opt-in, not the default ...)
So my current approach is everything should be as local as possible, as immutable as possible, etc. Basically Rust except I'm not a fan of low level programming. (I basically want Rust With GC (C# memory model), which sends Rust folks into paroxysms!)
I want it stricter than Rust in many respects, but also less annoying. (Better ergonomics and higher level, with a low level escape hatch when needed.)
Swift is apparently close to that, and might deserve another look.
I've also been obsessed with formal verification and proofs except, today I had a very revealing experience. I had an LLM incorrectly implement a major feature, and "verify" it with several thousand lines of tests. It was, as implemented, backwards, and also completely pointless — but all tests came back green!
I laughed when I realized, if it had been done in Rust, and with a layer of formal verification... well all the proofs (of the stupid and wrong and backwards thing) would have come back green too... It would have mathematically proven that the incorrect thing was correct...
Coincidentally, you reminded me of one of my favorite Charles Babbage quotes:
> “On two occasions I have been asked, ‘Pray, Mr. Babbage, if you put into the machine wrong figures, will the right answers come out?’ I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question.”
I suppose catching that kind of mistake is how humans prove to our future AI overlords that we should be kept around.
> Algebraic effects with deep, multi-shot handlers. A handler can resume a computation zero, one, or many times, which is what makes exhaustive search and exact inference ordinary library code.
I love me some algebraic effects, but this sets off alarm bells for me.
Multi-shot effects are neat and powerful but are incredibly difficult to reason about for humans, and given that there are few languages that have implemented them (and they're so niche with very little training data) I'm skeptical that LLMs are sufficiently better at them to make up the gap.
One-shot effects are a cross between `throw` and a function call. Multi-shot are full-on delimited continuations and come with all the complexity that entails.
I had a very similar thought and ended up building a capability system[1] in my language to capture side effects.
[1] https://march-lang.org/docs/cookbook/capabilities/ * docs are a work in progress
I’ve been very fascinated by the concept of a programming language designed for LLMs, both to that advantage of their strengths and to try and minimize their weaknesses.
Here’s a take I experimented with last year (feel very free to steal anything useful): https://github.com/GoogleCloudPlatform/aether/tree/feature/v...
(Note: main has a version that was an ugly syntax, the branch in the link was for a prettier attempt)
> and the runtime requires explicit permission to touch the filesystem, network, etc
This feels like more of an OS problem (or library problem) than a language problem.
> Run one program against many worlds. The same code can run against the real network, a scripted fake, a recording of last week's traffic, or a probability model of how servers usually behave
How is the "world" model different from plain dependency injection?
In addition to what the other comment said, this "world" model is great for hermetic testing of complex code, LLM written or not. We've seen existing projects that intercept the OS level syscall for testing, replayability, etc. Building it into the language runtime, hopefully with better ergonomics from the start than a syscall, would be a welcome addition broadly.
What effects provide beyond DI is entirely in their ability to abort (resume zero times) or (in the case of multi-shot effects) resume multiple times. An effect that resumes exactly once is structurally the same as a dependency injected lambda.
Yeah agree, what I really want to see now, is a programming language for LLMs, designed by a human (although code could still be LLM-made I suppose), and see how both of them fare in various scenarios.
But basically world is a bit more narrow, that moment where your code touches the outside world (logging, http, etc), you can swap that. It's sorta like DI but deliberately narrower, only the moments where code touches the outside world are swappable.. With DI in theory you can replace anything, which has its benefits, but at least personally I am not a big fan of mocks, except when they touch the outside world. So that's what's replaceable.
Fricking training distribution/same-y ness coming for us all… cool project though.
it would make it easy for humans to easily stub out tests with a docstring description and the tests that would guarantee certain behaviors. for the machine, it'd make it easy to add in new tests because the function+tests are in the same context window
Given how many useless unit tests Codex just loves to write, no, thank you.
Thankfully, its training data completely misses this. So at least for now it completely ignores doctests (at least in Elixir).
Anything we make gets to participate in this evolutionary process, even if it sounded dumb at the outset. In fact, doing dumb things is how we get "unstuck" from outdated ways of thinking.
I can get an OK tool that still goes a good distance in scratching an itch in say ~3-8 prompts, so with 1000 I'm looking at a small app. With 100000... I'm finding it a bit hard to imagine TBH; somewhere in the region of the Bun port to Rust[0] is my likely-off-base-but-not-as-bad-as-yours guess. Heck just consider that there are devs out there running systems with local models that are probably more than half the size of a frontier model, and how that 3000-hours-equivalent cost would've been eating into their pockets in the form of electricity bills.
[0] https://bun.com/blog/bun-in-rust
https://github.com/jbwinters/jacquard-lang/blob/main/docs/SK...
Agents I've tested with have had been able to pick up the language from that, at least to the extent that I've been able to test so far.
Building something like haskel's hoogle seems like a smart approach to this problem.
Whats different to the effects system just being a type system?
Isnt a function that opens a particular file still just a type? Perhaps dependent?
Reminds me of mercury which has determinism of the function like type signatures.
The effect system here is part of a type system (technically a type-and-effect system). Where a value type typically describes what value a computation returns, an effect describes which operations it can perform during evaluation.
The difference is that effects propagate through the call graph, so lower-level code cannot access disallowed resources without that authority appearing higher up. At runtime, world effects also require an explicit grant. In a typical value type system, lower-level code can introduce side effects without them appearing in the caller’s type.