이미 디펜던트 타입 함수형 언어로 수학을 코딩할 수 있었네요;;
방금 범주의 정의를 Coq로 코딩한 걸 보고왔어요.
예전에 잘 알지도 못한 채 나대서 정말 죄송합니다.

요즘 디펜던트 타입 언어는 아니지만 함수형 언어의 컴파일러를 만들고 있는데 졸업할 때까지 해도 완성 못할 것 같아요. 이론은 알고 있는데 구현을 못하겠어요. 마치 개념은 아는데 연습 문제를 못 푸는 것처럼요.
훨씬 어려운 디펜던트 타입 언어는 죽었다 깨나도 못 만들겠죠.

이제서야 제가 얼마나 ㅂㅅ 같았는지를 알 것 같습니다. 뭐든지 말로는 쉬운데 직접 하면 어렵네요. 수학도 그렇고 코딩도 그렇고 못할 놈은 못하는 것 같아요. 예전에 갤 어지렵혀서 죄송하고 용서를 구합니다.

- dc official App