Microsoft Research, 증명 지향 프로그래밍 언어 F* 발표
2024-12-25
F*(에프 스타라고 발음)는 순수 함수형 프로그래밍과 부작용이 있는 프로그래밍을 모두 지원하는 범용 증명 지향 프로그래밍 언어입니다. 종속 타입의 표현력과 SMT 솔버 및 전술 기반 대화형 정리 증명에 기반한 증명 자동화를 결합합니다. F* 프로그램은 기본적으로 OCaml로 컴파일됩니다. KaRaMeL 도구를 사용하여 F#, C, Wasm으로 추출하거나 Vale 툴체인을 사용하여 어셈블리로 추출할 수도 있습니다. F*는 F*로 구현되고 OCaml을 사용하여 부트스트랩됩니다. F*는 GitHub에서 오픈 소스이며 Microsoft Research, Inria 및 커뮤니티에서 적극적으로 개발하고 있습니다. Mozilla Firefox 및 Linux 커널 등 다양한 프로젝트에서 사용되고 있으며, 보안, 암호화, 시스템 개발 분야에서의 응용을 보여줍니다.
더 보기