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...

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.