It'll be interesting to see how the timing is enforced. Can you just set up your own NTP server to fool your phone into thinking it's really the future (and not just you adjusting your phone's clock manually). Will Google run a clock that you have to get a timestamp from (would it be easy to setup your own MITM proxy to get around this?). If the time somehow jumped backwards, would you lose the ability to install apps? Can google remotely disable this after it's already enabled (I think yes)?
I think it would be a bad idea to require an internet connection (for one thing, you might want to write your own app that does not require a internet connection); but, even if it doesn't, would not mean you can set the clock to avoid the delay, because it could be made to reset the delay if the clock is set.
They're not doing so here, but shipping a wasm-compiled binary with npm that uses node's WASI API is a really easy way to ship a cross-platform CLI utility. Just needs ~20 lines of JS wrapping it to set up the args and file system.
There's no such thing as a truly "cross-platform" build. Depending on what you use, you might have to target specific combinations of OS and processor architecture. That's actually why WASM (though they went with WASI) is a better choice; especially for libraries, since anyone can drop it into their environment without worrying about compatibility.
I think GP's point is that instead of having 3 target-specific rust-built binaries, they have 3 target-specific node binaries running rust-built wasm plus wrapper code.
That's essentially correct. Extraction is a term in roqc. A rocq program contains both a computational part, and proofs about that computation, all mixed together in the type system. Extraction is the automated process of discarding the proofs and writing out the computational component to a more conventional (and probably more efficient) programming language.
The original extractor was to ocaml, and this is a new extractor to c++.
Is early termination the only supported side effect? Its name suggests a more general capability, but I didn't see more examples in my (cursory) look at the readme
Early termination is the most common use case, but it’s not the only thing SideEffect represents.
The name is intentionally a bit broader — it’s meant to model “effects where normal composition should stop”.
In practice, that includes things like validation failures, logging or notifications at pipeline boundaries, and error reporting or metrics.
That said, the scope is deliberately conservative.
SideEffect isn’t meant to be a general-purpose effect system.
If it were, it would quickly turn into something very close to a monad or effect framework, which I’m intentionally avoiding.
reply