[일반] 따라 쳐봤습니다.

[기괴공학도(mecheng98)]

정말 놀랍고 신기하군요.

이런 걸 만들어보고 싶었는데,

직접 작동시켜 보니까,

죽었다 깨나도 못 만들 것 같네요.

(이런 걸 어떻게 만들었지? 삶의 목표가 없어짐 ...)

아무튼 좋은 걸 알려주셔서 감사드립니다.

[익명(124.51)]

coq는 어떻게 공부하심?

[기괴공학도(mecheng98)]

저도 잘 몰라요. lp님 코드 따라 친 거에요. - λ

[lp(24.3)]

조금 첨언하자면 Coq는 정리 증명기 중에서도 상당히 무겁고 기능이 많은 편입니다. 기초론과 구현의 선택에 따라서는 Coq 코드베이스의 100분의 1 이하로도 표현력 측면에서는 거의 동등한 시스템을 구축 가능합니다. 실제로 이를 연구 주제나 취미로 삼는 개인들도 적지 않죠.

[lp(24.3)]

게다가 이런 미니멀한 접근법이 Coq 같은 industrial-strength 증명기에 비해 꼭 열등한 것도 아닙니다 (이 분야에서 정답이 뭔지는 아직 아무도 모른다고 보셔도 됩니다). 그러니까 Coq 같은 사례 하나만 보고 좌절(?)하실 필요는 없을 듯.

[기괴공학도(mecheng98)]

그래도 Coq를 열심히 배워놓아야지 저만의 증명보조기를 구현할 때 도움이 되겠죠? 일단 형식언어부터 공부하고 있습니다. 첨언해주셔서 감사합니다. - λ