MS리서치·Inria의 증명 지향 언어 F*, 암호 라이브러리로 Firefox·리눅스 커널까지 진출

기존 C 코드베이스를 점진적으로 F*로 옮기면서 외부 라이브러리 호출을 표현할 수 있어서 좋았음. 꽤 탄탄한 언어임.

홈페이지 5페이지나 뒤졌는데 코드 예제 하나도 못 찾음. 새 언어 사이트라면 문법이 어떻게 생겼는지랑 왜 써야 하는지부터 보여줘야지, 증명 로직 설명이랑 문법 예시부터 앞에 두라고.

그냥 스크린샷 클릭하면 튜토리얼 나오는데?

Learn F* 섹션에서 링크 2개밖에 안 눌렀는데 튜토리얼 페이지 바로 나오던데.

비유를 빌리자면 F*는 프로그래밍 언어계의 던전 크롤러 같은 존재라, 아직 준비 안 된 사람한테 스크린샷 보여줘봤자 더 헷갈리기만 할듯.

난 반대로 언어 사이트 가면 유스케이스, 메모리 모델, 타입 시스템, 컴파일 타겟, 데이터 레이아웃, 제어 구조부터 알고 싶고 문법은 인덴트 기반인지 아닌지만 마지막에 확인함.

링크 하나 클릭했는데 온라인 북에서 코드 천 줄은 나오던데 무슨 소리야.

F*(에프 스타)라고 발음한다는데, 그건 아니지 않냐 (욕설처럼 읽힘).

F*는 사실 서로 다른 언어랑 증명 시스템 대여섯 개가 합쳐진 것 같음. 뺄셈이나 u8 같은 기본적인 것도 Lean처럼 제대로 처리 못하는 거 아니냐.