Re:Project Everest: Efficient, verified components for the H...
by xfer on Tuesday July 11, 2017 @04:55AM
(#14742591)
I don't understand these comments, you have no idea what F* provides for this project to work, but yet you can somehow perceive that rust would be a good language for this project. Really?
Re:Project Everest: Efficient, verified components for the H...
by catalin_hritcu on Tuesday July 11, 2017 @09:05AM
(#14743803)
Rust is a cool language for safe low-level programming with concurrency, but it is not targeted at program verification. F* can also do safe low-level programming by extraction to C, while also verifying that the code is functionally correct and secure. That's of course a lot more work, but also a lot stronger than the kind of guarantees one can get informally in rust (e.g. memory safety).
Re:Project Everest: Efficient, verified components for the H...
by andrewflnr on Tuesday July 11, 2017 @12:55AM
(#14741660)
F* is significantly more hardcore than Rust. Dependent types, refinement types, and effects are powerful features it has that Rust doesn't. I do a bit of Rust myself, but the world would probably be better if Rust was only a stepping stone toward languages like F*, Idris, ATS and friends. :)