News for hackers. Stuff that matters.
Re:Project Everest: Efficient, verified components for the H... by vorotato on Monday July 10, 2017 @05:24PM (#14739832)
F* is actually the reason I became interested in F#. So coool
Re:Project Everest: Efficient, verified components for the H... by spartanatreyu on Monday July 10, 2017 @08:26PM (#14740734)
I'm completely unfamiliar with F*, but it seems to me (even though it's still maturing) that rust would be a good starting language for this project.
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. :)