gf000

Formal verification proves if your specified theorem is correct. You can state any number of properties, in one extreme you just have basic types.

The interesting, 'hard-to-wrap one's head around' thing is that this verification is done by basically comparing arbitrary computations for equality.

So to prove that `3+3 == 6`, you would create an object with the type being `3+3 == 6`. And the rules of these languages are such, that the only way you can ever create an instance and thus a valid object for this type is if it's a true statement. 3+3==7 has no instance and can never have. (Interestingly, the instance of the above type is called `refl` for reflexivity. This is the only instance possible, and its type is basically a generic expecting a type, and a value of that type (this is where dependent types come in). Its "constructor" will place a single value into both slots, so the only way it can ever be instantiated is via values that the language/compiler itself considers equal.

A proof is just a manipulation of each "side" until they are trivially equal to each other).

One important caveat of the above: these languages evaluate expression not like most ordinary languages, like stopping at a thunk when the outermost value can't be further simplified. They will continue inward simplifying everything, and comparing these together - so even functions can be compared (though implementation matters a lot, and will alter the shape of proofs!)

Not the parent commenter, but most of it is surprisingly simple. You basically start with a "chat app" where you have a list of messages, send the whole conversation to an LLM and it replies back, which also gets added to the same list.

And you add a small twist, that instead of a 1-to-1 back and forth, you instead put it into a loop, where the LLM reply can itself "have a turn", e.g. a tool invocation, where your system is the one that replies (e.g. with the tool invocation's result). That's pretty much it, you have a 1 to potentially many "chat".

The harder part is getting all the "soft" parts right, like how to have well-behaving tool calls, timeouts, prevent huge cycles eating up tokens, but there are no one way to solve these, it's a fundamentally heuristic-heavy area.

Well, another way to put it is that the western markets managed to keep it out via propaganda and other soft influences on people.

Yeah, I love how people assume large powers have to do something. They are at most expected to do certain reasonable stuff (most of the time, a war is not beneficial to anyone so they try not to escalate that far), but there is not really global "law enforcement".

How can you steal something that won't materially be less from that? IP laws are cancer, and are definitely not in humanity's interest.

As opposed to finding some shady website with the same info?

Come on, nukes are not feasible to goddamn governments. The hard part is not "the science" behind it, the hard part is spinning stuff at such a high rpm that a tiny vibration will have the whole thing catastrophically collapse, that is refinement..

And basically every bad thing has already been available on the internet. We can't really do much about it, you can take out plenty of people with a single car, let alone biological weapons that are much scarier and easier to produce than goddamn nukes (which btw, even if you had one, what you do with it? Explode the neighborhood? Because you ain't transporting it anywhere meaningful, thats for sure. That ain't fitting your on-board bag on planes)

the couple multi-trillioners will have all the wealth of the world, and it will all crumble down

You mistyped it.

Then I buy a very expensive GPU rack and timeshare it with a couple of friends.

I agree, I personally really dislike discord - I do get that it works better for certain group sizes, but still.

Given that most of the clients are open-source, I wonder why signal or someone else didn't just change the "backend"

Well, I'm fairly sure that Telegram has substantially more users, so not getting spam is more likely due to that only.

How is that any better? Still no e2ee, proprietary, arguably worse UX for chat purposes.

For full-screen applications, Wayland has a protocol to let it display frames at its own pace - meant mostly for games for this very reason.

Humans are good at predicting stuff, and they can notice when the expected doesn't happen.

But I wouldn't necessarily say that people can notice it everywhere in every state of mind. The medium, context etc all matter a lot.

And for the complete picture, X is predominantly used with a compositor, so that same extra latency exists there as well.

But one is a "malloc allocation" and the other is a special "java allocation".

The two are apples and oranges and it makes no sense to compare them -- the latter is severalfold cheaper. Of course this comes at a price (read/write barriers, complex runtime, etc).

The context of this subthread is just to explain why someone who has Java experience might be prone to overcorrection when it comes to avoiding heap allocations

That's what I don't really understand: if anything, someone with Java experience should be prone to avoid heap allocation in something like Rust as it is more expensive on almost every other platform. This is what I'm talking about, and apparently I wasn't clear.

On the allocation happy path there is literally less work in case of Java. Like at least try to get what I'm saying and argue with that - I'm not saying that Java is faster or whatever, but that it has chosen different tradeoffs, and "stack vs heap" is an oversimplified model that doesn't help us understand the real performance impacts.

A pointer bump is a pointer bump, vs a malloc call that will try to find place, do some housekeeping, etc. And your Vec will need at least a single allocation, the backing buffer is not on the stack.

What "work" do we do needlessly? It's a pointer bump. With reclamation being no work. Comparatively a malloc call will have to do extra work to defragment.

Also, a stack is not a separate hardware element of the RAM, it's not faster than a sufficiently hot part of the heap - it just so happens that the current stack frame is pretty likely to be in cache.

Memory is memory, stack is not a unique hardware element. It just tends to be hot, but so can certain part of "the heap".

Of course this is a toy example, but were the compiler not smart enough (it is surely smart enough in this case) then the "too simple rust" version may actually be slower - it would allocate a Vec on the stack, but only a length, capacity and a pointer is stored there, the actual backing array is on the heap. Then it would create stuff on the stack, and copy over those bytes to the heap, object by object (it's a move).

Meanwhile the java version would have a continuous region of memory, next to it it would have objects, and it would just write pointers to said objects without moving/copying anything.

Surely enough rust is smart enough to optimize out this useless move in this case, but I think you are painting a way too simplified picture here.

Well, Minecraft sold far more and it's a scratch built 3d engine isn't it? Popularity is certainly not a technical achievement.

Java doesn't mandate the usage of a heap - it can in certain cases avoid doing so and allocate on the stack (escape analysis).

Besides, as mentioned java's allocations are much closer to something like using an arena in a low-level language, then a "slow" malloc. It uses thread-local allocation buffers, where you have a large buffer with a pointer pointing to the start of the free region. Allocation is just a pointer bump, not even needing synchronization since it is per a single thread. As it gets full, the GC moves out still alive objects in the background and resets the buffer.

This is pretty much the most efficient one can be after per-object type arenas and simply not allocating.

So can you in binary!

And that's more of a library ergonomics question how nice it is. There are plenty of other languages with nice ASTs and `eval`, and that's the only ingredient you need.

eval(parse(yourString))

No it doesn't

How is that different from other languages that have proper repls? Lisps don't really give you much here, if the language can parse itself and can eval it, you have the sufficient primitives.

What helps is how "small" the hot reloaded parts can get - lisps are good here due to a lot of functions and not much shared state. But that is again, not something specific to lisps, neither are they the best at it - there are far purer FP languages for example

But this is just not true. An utf8 string is most definitely not a bunch of cons cells. Having a one-to-one correspondence is not the same thing, and one might argue that a rust code snippet and the corresponding AST object is just as arbitrarily far apart with a clean one-to-one correspondence.

So like, what's the material difference between the two? You have a parse and an eval in both cases

Well, then ad absurdum it would be easier to just output a bunch of 0s and 1s, right?

The same goes for "just a list of nested lists", sure it is easy to produce it, and for trivial examples it may actually be easy, but for more complex and realistic problems lack of "higher order" structure is a negative!

For something like JavaScript, you can just have a language-native AST object with a few helper functions and then can just call "addFunction" on it with proper arguments so that the API shape validates plenty of properties of your output.

Given a new context, why couldn't the same model have a decent shot at reviewing some results? It's not like they identify whether this output is from them and then go "yeah correct", that's not how they work.

Well, my main point is not to never use macros, but that in certain cases a language-native feature that can also solve a problem you would use a macro for, it's probably better (better debugging, error messages, etc).

And my other point was macro systems in other languages, which I believe are better, in part due to not having homoiconicity, like Scala or rust.

Well, I was talking about the fundamental part. Of course you can have more practical implementations, like Scala or rust's macro system, that gives you a proper typed AST.

I mentioned in other comment that homoiconicity doesn't necessarily make writing macros simpler. It makes writing trivial toy examples simpler.

But let's compare it to a modern macro system like rust's or scala's, where you get a typed object representation of the AST, and for anything non-trivial you are better off with this latter.

Also, arguably the best is to have certain features in the language itself, that can be used to build proper abstractions - so you don't have to resolve to using macros in its place.