F*: 증명 지향 프로그래밍 언어
원제: F*: A general-purpose proof-oriented programming language
왜 중요한가
형식 검증 기반의 고보증 소프트웨어 개발 수요가 높아지는 가운데, F*는 암호화·클라우드 인프라 등 핵심 산업 분야에서 이미 실증된 증명 지향 언어로서 주목받고 있다。
Microsoft Research와 Inria가 공동 개발하는 오픈소스 증명 지향 프로그래밍 언어 F*(F스타)는 의존 타입과 SMT 솔버 기반 증명 자동화를 결합한 범용 언어로, Apache 2.0 라이선스 하에 GitHub에서 공개되어 Windows, Linux, Mac OS X용 바이너리를 정기적으로 배포하고 있다。
F*(F스타)는 순수 함수형 프로그래밍과 이펙트 프로그래밍을 모두 지원하는 범용 증명 지향 프로그래밍 언어다. 의존 타입(Dependent Types)의 표현력과 SMT 솔빙 기반 증명 자동화, 그리고 택틱(Tactic) 기반 인터랙티브 정리 증명을 결합한 것이 특징이다.
F* 프로그램은 기본적으로 OCaml로 컴파일되며, F#, C, WebAssembly(KaRaMeL 도구 사용), 어셈블리(Vale 툴체인 사용) 등 다양한 출력 형식을 지원한다. F* 자체도 F*로 구현되어 OCaml로 부트스트랩된다.
실제 산업·학술 프로젝트에서 폭넓게 활용되고 있다. 암호화 라이브러리 HACL*는 F*로 작성되어 C로 추출되며, 그 코드는 Mozilla Firefox, Linux 커널, Python, mbedTLS, Tezos 블록체인, ElectionGuard 전자투표 SDK, WireGuard VPN 등 다수의 프로덕션 환경에서 사용 중이다. 또한 바이너리 포맷 파서 생성기 EverParse는 Azure 클라우드 플랫폼의 Windows Hyper-V에서 모든 네트워크 패킷 처리에 활용되고 있다.
학습 자료로는 온라인 교재 「Proof-oriented Programming In F*」가 지속적으로 업데이트되고 있으며, 브라우저 내 예제 실습도 지원한다. 커뮤니티는 GitHub Discussions 및 Zulip 포럼을 중심으로 운영된다。