> 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 a day ago | parent | next [-]

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 a day ago | parent [-]

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 a day ago \| parent \| next [-]
		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.
	▲	a day ago \| parent \| prev [-]
		[deleted]

▲

lolinder a day ago | parent | prev | next [-]

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 a day ago \| parent \| next [-]
		> 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. [1] https://march-lang.org/docs/cookbook/capabilities/ * docs are a work in progress
	▲	jbwinters a day ago \| parent \| prev [-]
		That’s a fair concern. I’d expect multi-shot handlers to be relatively rare and mostly something library code uses rather than a day-to-day utility. But an LLM given free rein may decide to behave differently. For now, I am looking into making a clearer distinction between one-shot and multi-shot handlers so we can reject cases where resuming again would be unsafe, like around filesystem writes. More to explore here, certainly.

▲

fwip a day ago | parent | prev [-]

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.