4 ms·

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

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?

ehsanu1 9y ago
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).
- eastWestMath 9y ago
  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.
perrylaj 9y ago
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.
rhaps0dy 9y ago
>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.
- skolemtotem 9y ago
  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.
masklinn 9y ago
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.
kibwen 9y ago
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.
ridiculous_fish 9y ago
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.

ehsanu1 9y ago

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).

eastWestMath 9y ago
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.

perrylaj 9y ago

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.

rhaps0dy 9y ago

>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.

skolemtotem 9y ago
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.

masklinn 9y ago

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.

kibwen 9y ago

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.

ridiculous_fish 9y ago

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.