Hacker News Reader

Comment by faitswulff | Hacker News Reader

One thing I've been confused with about transpiled languages is how does correctness transfer? How do types or lifetimes etc. transfer to WASM, for instance? Or does it just depend on the correctness to be verified in the pre-compilation/transpilation stages?

View on HN

Correctness is typically checked long before code generation happens. This does mean the code generation backend must be trusted, whether the target be x86 or wasm. Just as you have to trust CPUs to not expose processes' memory to each other (oops).

Typed assembly is a thing - it’s mainly to ensure the compiler itself is correct, but it does give stronger guarantees. I think Frank Pfenning at CMU has written a language that’s dependently typed all the way down - so it’s IR and assembly are both dependently typed.

edit: I misread the question, my comment was geared toward languages transpiled to JS.

It's compile-time safety. Virtually none of the type knowledge exists in the runtime. Still, it's far better than nothing, with the self-documenting nature of typed code being one of the biggest wins IMO.

>how does correctness transfer?

The same way it transfers when the language is compiled to x86 instructions! By adding a pre-written and pre-compiled runtime.

No correctness isn't usually ensured with a runtime in these languages with stronger type systems, it's usually done with static analysis on an intermediate representation at compile-time.

WASM gives you a linear memory block and performs only bounds checking. It provides very few higher-order abstractions.

For example, the way you allocate memory in WASM is to link in a malloc() implementation. This malloc lives in the same linear memory block, and so its internal data structures are vulnerable to being smashed, just like classical heap smashing.

One improvement is that the call stack is maintained externally, so it is not possible to stack-smash a return address. Still heap function pointers are vulnerable to a return-to-libc style attack.

Round and round we go.

Unlike typical assembly, WASM enforces strong guarantees around memory safety (which I'll argue is precisely what you want for something with a web browser's attack surface). This does imply a performance hit (conventional wisdom is that WASM will, at best, be half as fast as "native" code), but also insulates the user from the usual memory-related pitfalls of C. Code transpiled from Rust is forced to pay this price as well, despite Rust providing substantially stronger memory safety guarantees than C; fortunately if you're using Rust you'll probably be the sort of person who agrees that this is a good thing, because Rust still lets one drop into unsafe blocks and potential memory unsafety in untrusted code delivered over the network is pretty much a nightmare scenario.

Same way it does when compiling to C or assembly, the correctness is checked on the source and assume the codegen and platform you run on behave correctly (and fix/work around bugs which inevitably arise).

So the correctness transfers in the sense that the code the compiler output should always be correct.

Reply on news.ycombinator.com