F*란 무엇인가, 그리고 왜 주목해야 하는가
F*(F star)는 Microsoft Research와 Inria가 공동 개발하고 있는 증명 지향(proof-oriented) 범용 프로그래밍 언어다. 단순한 함수형 언어가 아니라, 의존 타입(dependent types) 과 SMT 솔버 기반 증명 자동화, 그리고 타틱(tactic) 기반 대화형 정리 증명을 결합한 것이 핵심이다. 순수 함수형 프로그래밍뿐 아니라 부수 효과(effect)가 있는 프로그래밍도 지원하며, 언어 자체가 F*로 구현되어 OCaml로 부트스트랩된다.
백엔드 개발자 관점에서 흥미로운 점은 다양한 컴파일 타깃이다. 기본 출력은 OCaml이지만, KaRaMeL 툴체인을 통해 C나 WebAssembly로도 추출할 수 있고, Vale 툴체인을 이용하면 어셈블리 코드 생성도 가능하다. 보안이 중요한 저수준 시스템 코드를 수학적으로 검증된 형태로 작성하고 싶을 때 실질적인 선택지가 된다.
실무에서의 연관성 — 형식 검증과 정확성 보장
일반적인 Java 웹 백엔드 개발에서는 단위 테스트나 통합 테스트로 코드의 정확성을 검증한다. 하지만 테스트는 "특정 입력에서 올바르다" 는 것만 보여줄 뿐, "모든 경우에 올바르다" 는 것을 보장하지 못한다. F*는 이 간극을 메우는 접근을 제시한다.
F*에서는 함수의 타입 시그니처 자체에 사전·사후 조건(pre/post-condition)을 표현할 수 있다.
val divide : x:int -> y:int{y <> 0} -> Tot int
let divide x y = x / y
위 예시처럼 y <> 0 조건이 타입 레벨에서 강제되므로, 0으로 나누는 상황은 컴파일 타임에 원천 차단된다. 이는 런타임 예외를 줄이는 것을 넘어, 시스템의 정확성을 수학적으로 증명하는 개념이다. 암호화 라이브러리, 프로토콜 구현, 보안 크리티컬 컴포넌트 개발에서 이미 실제 활용 사례가 존재한다.
학습 경로와 생태계 현황
F*는 오픈소스(Apache 2.0)로 GitHub에 공개되어 있으며, Windows·Linux·macOS용 바이너리를 정기적으로 배포한다. OPAM, Docker, Nix 등 다양한 설치 방법을 지원하므로 로컬 환경 구성의 진입 장벽은 낮은 편이다.
학습 자료로는 "Proof-oriented Programming In F*" 온라인 북이 지속적으로 업데이트되고 있으며, 브라우저에서 바로 예제를 실행해볼 수 있는 인터랙티브 환경도 제공된다. 저수준 코드 작성에 관심이 있다면 C로 컴파일되는 F*의 서브셋인 Low* 튜토리얼도 별도로 준비되어 있다. Oregon Programming Language Summer School, ECI 등 학술 행사에서 강의와 코드가 공개되어 있어 체계적인 학습도 가능하다.
정리
- F*는 의존 타입과 SMT 자동 증명을 결합해 런타임 오류를 컴파일 타임에 수학적으로 차단하는 증명 지향 언어다.
- OCaml, C, Wasm, 어셈블리 등 다양한 타깃으로 컴파일되어 보안·저수준 시스템 개발에 실용적으로 활용 가능하다.
- 테스트만으로 커버하기 어려운 "모든 입력에 대한 정확성 보장" 이 필요한 도메인에서 도입을 검토할 가치가 있다.