> 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?)
show comments
phildenhoff
Very cool -- I often thought that Unisons caching approach should be adopted more widely. Look forward to poking at it later!
wren6991
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?
show comments
sajithdilshan
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.
> 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?)
Very cool -- I often thought that Unisons caching approach should be adopted more widely. Look forward to poking at it later!
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?
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.
"Esperanto for Clankers"