derdi

I found Codex to use "gate" in a different sense: As the condition of an if statement. I have a local style rule not to use that. Another really grating thing is to use "X-shaped" for "something vaguely related to X". And using temporal words like "still" and "already" in contexts with no temporal connotation.

I wonder how long this will still be a thing. More and more companies seem to come to the conclusion that tokenmaxxing is just too expensive for the value it delivers. Will there be others that continue doing it? Will there be companies that advertise "unlimited tokens" as part of job listings? How will they react when employees test the limits of "unlimited" (whether by accident or not)?

I would expect Postgres to be heavily tested with things like Valgrind and various sanitizers. I'd be surprised if there were low-hanging fruit. But also, if there is code that does something fishy with pointers, wouldn't the AI likely paper over it by adding an unsafe block in the Rust version, preserving the same fishiness? It's hard to know how hard it would try to prove that the original is broken.

I know how to write a test that verifies other tests. But I can do that already, I'm wondering what Beagle would add.

I also know that if the meta-test is writable to the agent, it will change it if it feels like it wants to get rid of some other test. Even if it can't change the meta-test, it can hollow out existing tests to make them pass trivially.

I don't think nondeterminism is the problem. The problem is following rules: If I tell the agent not to change tests, it can conveniently "forget" about this. It doesn't much matter if it forgets deterministically. The problem is that it can forget at all.

Thinking about this more, like every blockchain, this only makes sense if there is an incentive to publish each log entry as quickly as possible. Once it's published, of course it's tamper-proof, including against "the operator of a recorder can delete the bad day". Presumably the incentive to publish and the protection against the operator choosing to "never write a record at all" is the same: You must get paid for publishing a log entry. Because a log entry is, quite literally, "proof of work".

But if you're incentivized to publish as quickly as possible, then your customer gets the log immediately, and there is no need for a "trusted" third party to act as a "witness" and seek rents for not doing anything useful.

And none of the above protects against the vendor using your sensitive data to (a) do the work as contracted, with a cryptographically verified log and everything, but also (b) copy/analyze/abuse said data without telling you.

It's 2017 again, and someone on HN is inventing "blockchain for X", poorly. (Also note that it doesn't matter what kind of work X is, except for aligning this with HN's current main interest.)

> Disclaimer: this proves integrity, not completeness (as a self-held chain proves nothing was edited but does NOT prove that nothing was omitted).

Or as the page puts it in more detail:

> A self-held chain proves integrity: nothing was edited or reordered after the fact. It cannot prove completeness: the operator of a recorder can delete the bad day and re-seal the chain, or never write a record at all, and the chain stays internally consistent.

I don't get this. If I "hold" the "chain" (I hate the jargon agents invent), why can't I edit or reorder and then "re-seal" it?

See my reply to the sibling. Yes, it matters that the outcome is a working system! It doesn't matter whether the system was created by a human pressing keys on a keyboard.

This 6-minute video (linked from the website) demoes it nicely: https://www.youtube.com/watch?v=qnIu-Xu64H0

It sets up a bunch of panes for you and tracks your agents' status and everything is clickable. You could probably do much of the same by setting up tmux appropriately. Or you could use this, which is already set up.

I tried herdr today, and it's not bad. Better than my previous many terminal tabs. Copy-and-paste is wonky (and it's ridiculous that copying is documented in multiple places in the docs, but pasting is never mentioned). And when an agent is waiting for a shell command, it shows as "idle", which IMO is wrong. Still, seems OK so far, I'll stick with it for a while.

I don't think processes have to be deterministic. Results should be, in the following sense: Both humans and LLMs should write software that is well-written, well-tested, well-documented, and that meets the spec. But this still leaves a lot of room for creativity (or rolling dice).

Thanks! I actually find human-written text very refreshing compared to what I have to read all day. I'll stay tuned.

Humans aren't deterministic. Determinism is a red herring. There are lots of other problems with agentic programming, but this is not at the top of the list.

This is a very interesting introduction to a blog post, but... I'm somehow missing the actual blog post. How does this stuff work in practice? What are some concrete examples? How does one get from JavaScript tokenizing things in a commit hook to validating that the LLM didn't disable tests it didn't agree with, or any other helpful property?

Agreed that the napkin is pretty unclear. You can check the reference VM for clarification of the de facto intended semantics: https://github.com/adriancable/eternal/blob/main/vm/vm.c

> Tokens billed at API prices are profitable for openAI and anthropic today

That's nice for them. What's less nice for them is that big customers are figuring out (some faster, some more slowly) that they don't want to pay API prices, or at least only for a much smaller number of tokens.

No, the clue is people realizing that relying on the tools costs too damn much. The tools may be fine-ish for what they do, but there might be a bubble built on unrealistically high expectations of revenues.

For here (and the website), I would be more interested in trustworthy information about what is actually verified at compile time, and what happens when verification fails.

What if you write a function that takes an array (as an array type if you have one, or as a pointer, or a slice, or whatever). It returns `array[0] + array[1]`, but it has no bounds checks in the code, neither as actual `if` statements nor as `requires` clauses.

Verification of such a function must fail at compile time, right? Does it? What does the error message look like? Someone else found some quote somewhere that seems to suggest that integer overflow checks are implemented as runtime checks if you can't eliminate them at compile time. Does that also happen for bounds checks? If yes, does the user get a warning saying that M out of N checks were moved to run time?

It's just really unclear if you are really doing "Verified safety without the runtime cost." or if you have reinvented Java, which will be just as good (actually better) at eliminating these bounds checks as compile time.

The more interesting loop invariants aren't the ones about the loop counter but about the contents of the array. If you require `forall i, array[i] == value` after that loop, will the system come up with the loop invariant about the prefix of the array for any given `i`? What about something like bubblesort or insertion sort?

I was confused by the matrix multiply example since it doesn't show requires clauses. So I looked at what is presumably the source I'm supposed to look at: https://github.com/bneb/lattice/blob/main/basalt/src/kernels...

There's a comment saying every function in that file has requires clauses, but... They don't?

Also, the actual implementation of matrix multiply is manually tiled, while the website boasts about automatic loop tiling. It's hard to know what to trust here.

I didn't look at the details you posted, but as a compiler engineer, the general statement doesn't surprise me. More complex control flow can block optimizations. Many compiler optimizations involve duplicating code in some way (loop unrolling, for example). Hence, more complex control flow can block optimizations that would increase code size.

Yes. You are correct. You completely missed the point of what this subthread is about, but yes. It's clear what "subject to the laws" means to normal people.

So people on a work visa are "subject to", specifically because of two criteria (income tax and conscription) which must both hold, at least hypothetically? What if the US passes a constitutional amendment explicitly saying that foreigners on work visas cannot be conscripted, would that, by removing the hypothetical, have the implicit effect of making such people no longer "subject to" its jurisdiction?

I think your take on this is overly complex and silly.

Can you expand on the harm of degrowth? I usually see it framed in terms of "our state retirement system is an obvious pyramid scheme that is about to collapse, we need to keep the scam going as long as we can". Are there better reasons to worry?

"X is bad" is obviously not a license to commit genocide to lessen the effects of X.

Easy, very affordable access to birth control (both information and actual physical stuff) for all humans is a very good idea.

IANAL, but it seems to me like the US could totally pass laws regulating Germans on German soil. It just couldn't enforce them in US courts (short of kidnapping Germans from German soil, or luring them to the US somehow). So it would be mostly pointless but not impossible.

Also, multiple countries have laws claiming universal jurisdiction. As I understand it, French laws against genocide denial claim to apply universally.

From your own discussion, it seems like "subject to the jurisdiction" should be understood as "can be judged in court". Diplomat is immune = can't be judged = not subject to jurisdiction. Immunity lifted = can be judged = subject to jurisdiction.

What if you're in the US on a work visa, so you do expect to pay income tax but don't expect to be conscripted into military service? What's the correct preposition for that case?

One problem with the "won't happen in production" argument is that humans are demonstrably bad at predicting "won't happen in production" situations.

Oh no, you have just proved formal verification useless! Or, if you have an outer event loop that should potentially run forever, you mark only that one loop accordingly (details depend on the system).

Nitpick: You don't necessarily need any specification at all in order to reap benefits. Formal verification languages come with a lot of conditions that your program must fulfill in order to be accepted: Every loop terminates, every object you want to read/write is non-null, every list or array access is in bounds, etc.

For example, if you load an arbitrary C program into Frama-C, you'll have tons of properties to prove before you can even think of adding your own specification. The promises you get is that the program will always terminate and will never invoke undefined behavior. These properties are extremely useful, and these requirements are unlikely to change! And yes, C is... special. But pretty much any language has lists or arrays, nullable/option types, and unbounded loops. "No crashes/panics/uncaught exceptions" should be worth it.

And then, even absent a specification, you can start modeling invariants of the system anyway. This list is always sorted, this number is always strictly positive, this data structure never contains duplicate entries, etc. Anything that today would be a comment saying: "Important! The caller must ensure that..." This can help you gain confidence in your system. And if some day a requirement comes along that really requires you to violate one of these invariants, well, you can just remove it, the same way you would remove a test that no longer reflects something that should hold.

OK. You don't agree with the OP's "arbitrary lines", I don't agree with the OP's arbitrary lines, I still don't understand why you felt you needed to attack me for this. But I hope you have a lovely day.

I still have my first Jolla from 2014, I used it until... 2022-ish? My main gripe was that RAM was limited, the OOM killer killed my browser way too often while I was actively using it. I didn't use too much Android stuff, but as far as I remember it mostly worked. I'd expect this new one to work just fine.

The thing that sounds really fishy is the "User configurable physical Privacy Switch". If you can configure it in software (how else?), then it's software-defined. If it's software-defined, then it's not physical.