Hacker Newsnew | past | comments | ask | show | jobs | submitlogin
Project Everest: Efficient, verified components for the HTTPS ecosystem (project-everest.github.io)
75 points by EvgeniyZh on July 10, 2017 | hide | past | favorite | 5 comments


F* is actually the reason I became interested in F#. So coool


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.


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?


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


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




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

Search: