[질문] 그럼 증명언어의 단점은 무엇임?

[익명(223.39)]

하스켈 시플플 러스트보다
표현이 자유롭다면
단점은 무엇인가요? 성능?

[다믜(damhiya)]

배우기 어렵고 사용 하기도 어려움. 프로그래밍용으로 쓰면 성능이 좋진 않지만 성능 신경쓸거면 애초에 C같은걸로 짜고 증명언어로는 증명만 해야됨.

[익명(223.39)]

파이토치같이 c++로 성능 안떨어지게 하면서 쓸순없나요?

[익명(223.39)]

굳이 c++아니여다

[다믜(damhiya)]

Coq이나 Agda를 Ocaml, Haskell 등의 언어로 컴파일할 수 있음. 거기서 다시 FFI로 C/C++ 호출할 수도 있고

[익명(223.39)]

ㄱㅅ

[츄럴(118.235)]

거의 대부분의 프로그램은 증명을 필요로 하지 않는게 가장 큰 단점임... 증명 언어 할 줄 아는 사람 구하는 회사 한 번 차아봐여 얼마나 있는지,,,,

[익명(118.235)]

대부분의 회사는 DB 전자장부회사에요