Hacker News new | past | comments | ask | show | jobs | submit login

Going the long way is just a 'proof of concept' sort of thing. You could design a high-performance JIT around equivalent safety mechanisms, and even prove the tricky parts.



JavaScript's memory model is incompatible with that of Rust anyhow. You would want something like typed assembly language (Google this--it's a fertile research area). Very researchy though, with uncertain payoff.

But note that a lot of security problems are not in the jitcode but rather in C++ implementations of JS objects and in the compiler itself.


BOOM! Typed, assembly language is exactly what I was going to recommend! TALC assembly, Chlipala's Bedrock, and Microsoft's CoqASM are Google keywords to use for anyone following along.

CakeML or Verisoft's C0 could be useful for assembly generation but not as sure there. Tough constraints in JIT. Edited to add Myreen's JIT that I just remembered.

http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=F58...


CoqASM looks interesting! Is it publicly available anywhere?


Not that Im aware of. They might privately license it if asked. I mainly bring it up as something worth cloning by FOSS team given there's plenty details in paper. Meanwhile, look up Magnus Myreen's publications and software as they're on a row with verified everything.


Typed assembly language would be an excellent addition to the Rust ecosystem -- there are still segments of software which should (or must) be implemented in assembly, so anything that can help make assembly easier to verify would be helpful to the ecosystem.


In theory, but there isn't even good research on this, AFAIK. Fast JITs for languages like JavaScript require unsafety in the state of the art today.


I'll believe it when I see it. :)




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: