간단한 파서랑 체커를 verified programming 으로 짜야 할 일이 있는데


대충 언어를 저 정도 생각해보고 있는데 혹시 써보고 비교 좀 가능한 사람 있음?


필요한 specification은 대충 디펜던트 타입만 쓸 수 있으면 다 표현 가능할 것 같음


대충 보면 F* 은 증명과정 대부분을 유저에게서 숨기고 자동화하는 극실용적 접근법이라서 


이걸로 필요한 증명이 다 되는 종류의 프로그램이면 정말 좋은데 그보다 더 강력한 증명기능이 필요할 때 애로사항이 터질 것 같고


로우레벨까지 모든 단계를 다 검증한다는 면에서는 CakeML이 제일 월등한 것 같은데 이건 배울 수 있는 리소스가 너무 없네


일단은 Agda 생각하고 있음