UncleEntity

I took a different approach with this JavaCard VM I've been working on, first I had Claude implement the VM from the spec and then I had it implement a proof generator (also from the spec) so an identical bug would have to exist in both of them to make it through. Worked pretty well, the JCVM and bytecode verifier are both statically verified using ESBMC (which found a few bugs in that project so, win, win).

Now I have it working on a verifier for the bytecode transformations the optimizer uses, also using the static verification approach, to discover them all and ensure they are all valid. This one is seeming to be on track to making it fast enough to work on a real grammar as opposed to the 'academic grammars' the literature typically uses to prove the lemmas. Claude seems to be fighting this and has been working on the same refactor for over a week now so, we'll see...

Yeah, the more ambitious I get the more Claude doesn't follow the plan and just makes up random stuff to get the tests to pass instead of following the design...

I'd like to see the UCLA study which showed that in states that legalized marijuana, bankruptcies and credit card delinquencies increased about 25%.

Admittedly, I didn't read the whole article but I didn't see anything about banning social media and/or putting pot stores on every corner to compete with the liquor/tobacco stores. Seems like something they would have put in the beginning to draw the reader in, dunno?

What I do know from living on this planet for over half a century is that gambling and alcohol and certain drugs are very addictive and have the tendency of ruining people's lives. Pretty much common knowledge at this point, one would have thought...

The problem I've been having is the LLM's are super dodgy, not even ten minutes ago the 'solution' to a proof failing was to disable that check in the static analysis harness so the tests pass since their first try (with a counter example and lemma from the literature in hand) didn't fix the issue.

Maybe it's an issue because it controls both sides of the fence and can change things willy-nilly when it thinks I'm just watching the youtubes but I haven't been able to find a another way to do this so, here we are...

>> I was curious why you swapped over to a register based VM

Not the OP but there are real performance benefits, I've been poking at a wasm VM and it has two jit backends where one is pure copy-and-patch while the other caches the locals in registers using the function args + copy-and-patch and there is a significant performance gain just from that alone. A push/pop from a stack is fairly expensive while the register caching keeps things in the CPU's happy place. The smallest gain was ~2x over the interpreter on memory bound tasks while the largest was ~20x on math heave kernels. Admittedly, the interpreter isn't the fastest thing ever as its one and only goal is conformance with the spec to use for differential testing but the difference between the the two jit levels are somewhere in the neighborhood of 1.5-5x depending what the code is up to.

The three biggest performance gains, from the random benchmarks, are quality of the bytecode out of the compiler, the jit itself and register caching from what I can tell from the fancy chart I had Claude make and a good squint. Tail-calling would be somewhere on that list too but I can't measure that as all the opcode do the tail-calls between each other as that's just how it was all put together, the code the interpreter runs is the same code the copy-and-patch jit stitches together as they are both generated from the same DSL. Which is also the biggest cost with the register caching as the code template file grew from tens of kilobytes for the 407(?) wasm opcodes to ~3MB for all the specialized ones to pass the locals in eight args but that's really just a binary size thing, the stitched together functions just pick and chose the ones they need.

Long winded way to say CPUs like when you keep things in registers, I suppose...

I thought this was just a thing until I moved from Cal to Arizona and people would get really mad about it until I asked someone at work and learned it's illegal.

My first motorcycle was fast enough to get out of the way of stupid drivers (and be fun) while my last one was so fast it still amazes me to this day that I'm still alive. Apparently it was amateur raced with all the things that entails, which is probably why I didn't die as it was so obnoxiously loud people knew there was a motorcycle around them so I couldn't really hide in their blind spots, not that I would ever do that because that's a quick way to get a free ride to the ER.

$2500 for a vehicle which could most likely top out around 200 mph probably wasn't the smartest purchasing decision I've ever made. The only smart thing I ever did was there was always something suitably wrong with it I never took it out into the desert to see what the real top speed was.

My Fiat 500 has the same size engine and keeps me out of trouble. And around the same MPG...

Yeah, that only works if they follow the plan (they don't), actually write the tests first (they don't) and don't silently defer anything which doesn't have a test written as "speculative without a use case".

Or just write tests to match the buggy code after you call them out for not writing tests.

I mean, the struggle is real...

No matter how weasel-proof you make the plans they are much better weasels and just do as little as possible and "the test not written is the test which never fails." There's a certain amount of zen to them.

Yeah, I used to work with a ton of “unhinged” people willing to take risks because it was the literal job requirement, being willing to jump out of a perfectly good airplane behind enemy lines, yet was completely optional as one has to both volunteer for jump school and could always refuse to jump with no real punishment... well, as long as you did the jump refusal on the ground and were willing to go wherever they decided to reassign you (Korea).

Even they didn't expect anyone to work seven days a week forever, we trained hard and were given plenty of downtime so nobody went (too) crazy.

Seems like they're trying to go back to the days of serfdom without the Sundays off bit...

> Native interop with JS objects on the JS GC heap isn't supported as well.

Isn't that what the i31 type is for, that extra bit is a tag for...something, native GC'd object perhaps? Not so clear on that myself as Java's object model (minus synchronized) slots in perfectly so my Java 1.0 -> wasm compiler doesn't need it but that's my limited understanding of what it's for.

I mean, I got them to 100% using the official conformance suite on my copy-and-patch jit compiler/interpreter WASM VM...

Saw that Salt Language article a day to two ago on how they do the static verification as part of the compilation process (or whatever they really get up to) and that's next on the agenda, tried that with a JavaCard VM I was poking at as its 'computation space' is much smaller but that was too much for my poor little laptop to handle but, apparently, this Salt thing is much different and actually tractable so, we'll see, still working out the details.

What I suspect is this 17% is the exact sub-set it needed to hack together to make the goal (running some example website) a reality as this is what those dodgy weasels do if you let them. Then you get to spend 200x the time to fill in the rest of the "speculative features deferred due to no real consumer" on top of whatever dodgy system they made up, which is usually whatever is easiest/closest to the literature instead of the actual intended design. Lots and lots of fun to be had doing the full-pipeline refactors to add that last 2% which need support from tip to tail.

It's all in good fun, though... probably?