일단 기능 구현이랑 스펙 기술은 다 끝났고 이제 스펙 증명하는 중

경쟁 언어들과 비교하면 프로그래밍 언어로서는 확실히 더 나음. 일단 컴파일러가 기본으로 독립 executable을 뱉어낸다는게 너무 좋다. 안 써본 사람은 믿기 어렵겠지만 저게 ‘그냥’ 안 되는 놈들이 검증 프로그래밍 언어에는 ㅈㄴ 많아서... 그리고 검증할 필요 없는 부분에는 하스켈 함수를 마구 끌어와서 떡칠해도 되는 점도 편함.

반면 증명 언어로서는 좀 많이 불친절한 편. Tactic 증명을 못하고 무조건 term 증명을 때려박아야 되니까 컨텍스트를 보고 내가 하고싶은게 뭔지 머릿속으로 알아도 그걸 실제 컨텍스트에 반영하려면 말 그대로 몸비틀기를 해야 됨. 아니면 보조 정리로 도배를 하거나. 그래도 방정식 컴파일러가 똑똑해서 증명할 필요 없는 경우의 수는 미리미리 컷해주는 건 좋더라.