F*: 증명 중심 프로그래밍 언어

F*: A general-purpose proof-oriented programming language

F*(F star)는 순수 함수형 프로그래밍과 효과 프로그래밍을 모두 지원하는 범용 증명 중심 프로그래밍 언어입니다. 의존 타입의 표현력과 SMT 해결 및 전술 기반의 대화형 정리 증명을 결합합니다. F* 프로그램은 기본적으로 OCaml로 컴파일되며, KaRaMeL을 통해 C, Wasm으로, Vale 도구 체인을 통해 어셈블리로 추출할 수 있습니다. F*는 Microsoft Research, Inria 및 커뮤니티에서 개발 중이며, GitHub에서 오픈 소스로 제공됩니다.