Been doing this at work for the past couple weeks. Extremely powerful to be able to have an agent open a PR with some experiments showing it makes some function faster using SIMD or CUDA, and just confidently merge it because the PR has a Rocq proof that it's behaviorally equivalent to the original implementation.
I'm curious about your workflow (or the one in the blog post), I have been doing some experiments proving things about existing binaries and it's been extremely slow progress.
Yeah it took a bit to decide which abstraction level to target but I ended up choosing LLVM IR (planning to try PTX soon). It's been pretty successful so far for SIMD stuff, although proving theorems about concurrent programs seems a lot slower so far.
No existing semantics are enough for my goals, so I'm building my own based on Vellvm, and proving "equivalence" theorems to it and other related work that specify what quirks/discrepancies/idiosyncrasies they have with respect to each other.
Ah, interesting. I went with Ghidra p-code which seems ok but what I didn't really appreciate going in was how much of the platform API surface you have to describe before you can prove pretty much anything at all.
having written a few extensions... they are basically the same API with a few differences you need to account for. there's polyfills that can unify the experience a bit more too.
Currently I remap all backgrounds, text, and vector graphics, and I leave raster images alone. This works great for documents whose only raster images are photographs; some documents do have other raster images that might even have white backgrounds instead of transparent, so that's not ideal, but it seems to work decently well in practice.
A bug in the scriptlet I used to post it, which truncated the title as
“Silicon Valley sees AI as the solution – for everyone els...”, which I didn’t notice had dropped the third line of the title.
> In case you are curious about Fable: I intentionally did not test it because I was not sure if the classifiers they are running might downgrade me to Opus silently.
Is this still a thing? I thought Anthropic walked back the silent downgrades so now all the different domains downgrade non-silently.
It's slower. Wasm32 can just reserve 8 GiB (32-bit pointer + 32-bit offset) of the virtual address space from the OS for each memory, so checking for out-of-bounds memory accesses imposes no performance penalty. Wasm64 can't do that, so each memory access is a bit slower.
Oh that's interesting, never noticed it in my experience but I have never written anything in wasm where it would matter. Makes perfect sense now that I think about it though. Thanks!
Sometimes I wonder whether it's possible to run the wasm code in a separate sandboxed process to eliminate a lot of checks. I mean optionally, because normally JS calls wasm code synchronously in the same address space. The bridge will add more latency when there is a transition between JS and wasm. It's obviously complicated because some data structures can also be shared, such as SharedArrayBuffer.
> The bridge will add more latency when there is a transition between JS and wasm.
This would be similar to how NaCl/PNaCl communicated with the JS side (via message passing), and that really sucked and would also be prohibitively slow for talking to 'high frequency APIs' like WebGL2 or WebGPU (or the DOM heh).
I've seen various posts about Elixir's gradual type system pop up on HN, but haven't been following too closely. Does anyone know whether this particular gradual type system can change the asymptotics of programs vs untyped code? As far as I'm aware, most gradual type systems (e.g. Racket) can make programs run asymptotically slower, although there are some exceptions [1].
Elixir's gradual type system cannot change the asymptotic complexity of your programs. The design explicitly rules out mechanism that causes slowdowns in other gradual type systems (runtime casts at static/dynamic boundaries)
Most gradual type systems insert coercions when values cross the types/untyped boundary (checking every element of a list, wrapping values in typed proxies, etc) but Elixir's team published a "strong arrows" result specifically to achieve soundness without those runtime checks. The bytecode the compiler emits is semantically identical to untyped code.
That can be a concern indeed but it is worth noting that strong arrows compose/propagate. So if you have a function without guards that calls a function that guards on said types, the caller is also strong! We will likely have mechanisms to measure "strength" when we introduce type annotations.
Is it fair to think of this as the ability for type information to be propagated in both directions, e.g. both up and down the callstack? So callees down the callstack may receive any type information the caller might have, while callers up the stack may also receive any information callees further down the stack might have? Please correct me if my understanding of what you wrote is way off base!
reply