News for hackers. Stuff that matters.

A comment on F* – A Proof-Oriented Programming Language. Parent comment

Re:F* – A Proof-Oriented Programming Language by daxfohl on Thursday May 16, 2024 @11:01AM (#40379257)
I remember reading (~10 years ago) that F* was created as part of a "Project Everest" a long time back, with the goal of creating a provable TLS implementation. I never saw that anything came out of that though. If it's that hard to create something as well-defined as a TLS implementation, it seems futile to think this could ever be used for hand-wavy things we encounter in day-to-day work, no? Or are there real-world use cases where this could really be applied?
[ Parent | on HN ]
Re:F* – A Proof-Oriented Programming Language by lambdanik on Thursday May 16, 2024 @11:14AM (#40379414)
F* existed before Project Everest, but Everest did power a lot of its development.

We have built verified systems and components in the TLS ecosystem, including parts of TLS, QUIC and related protocols, and continue to do so: https://project-everest.github.io/

Some of it is deployed in production systems:

* Verified parsers in the Windows kernel and elsewhere: https://www.microsoft.com/en-us/research/blog/everparse-hard...

* Verified crypto in Linux, Firefox, Python, ... https://github.com/hacl-star/hacl-star

[ Parent | on HN ]
Re:F* – A Proof-Oriented Programming Language by daxfohl on Thursday May 16, 2024 @11:58PM (#40386250)
So _would_ it possibly be useful for business apps? Or is that still a long way off?
[ Parent | on HN ]
Re:F* – A Proof-Oriented Programming Language by octachron on Thursday May 16, 2024 @11:16AM (#40379438)
The Everest project did publish a proved TLS implementation: https://mitls.org. And at least the EverCrypt* cryptographic primitives has been used outside of academia.
[ Parent | on HN ]