F*: A general-purpose proof-oriented programming language
5 hours ago
- F* 是一种面向证明的编程语言，结合了依赖类型、SMT求解和基于策略的交互式定理证明。
- 它默认编译为OCaml，并可通过多种工具提取为F#、C、Wasm或汇编语言。
- F* 在Apache 2.0许可下开源，可在GitHub上获取，并支持多种安装方式，包括二进制文件、OPAM、Docker、Nix或从源码构建。
- 学习资源包括在线书籍、Low*教程以及来自季节性学校的课程材料。
- F* 被用于工业和学术项目，如Project Everest、HACL*、ValeCrypt、EverCrypt和EverParse，并在Firefox、Linux内核、Python、Azure等领域有生产部署。
- 关于F*的广泛研究涵盖了语义学、效果、安全性、密码学、系统、解析和程序验证，并发表了大量学术论文。