[%] butterfly같은건 자체로는 흥미가 안끌림

[ㅇㄹ(rerereq)]

Rust chalk같은건 좀 끌리는데

[기괴공학도(mecheng98)]

러스트 인터프리터임? - 훈다리 훈다리

[ㅇㄹ(rerereq)]

아니 trait랑 struct로 프롤로그 같이 돌아가는거임

[ㅇㄹ(rerereq)]

나아중엔 컴파일러에 포함될 가능성이 있다고함

[기괴공학도(mecheng98)]

오 이미 있었구나 - 훈다리 훈다리

[기괴공학도(mecheng98)]

자연수에서 덧셈의 교환 법칙 증명 가능함? - 훈다리 훈다리

[ㅇㄹ(rerereq)]

그런 용도가 아니라 컴파일러가 쓸놈임

[기괴공학도(mecheng98)]

컴파일러가 컴파일하는 데 쓴다고? 원래 Butterfly도 메타인터프리터인데, 이걸로 증명보조기 타입체커 만들려고. - 훈다리 훈다리

[ㅇㄹ(rerereq)]

예를들어 T: Clone이 돼야된다던가 T에 u32이 들어갈수있다던가 이런거 추천해주는거

[기괴공학도(mecheng98)]

아무튼 원래 Butterfly가 시시한 언어이지만 타입체커로 쓰일 수 있을만큼 강력하다고! 무시하지 말라고 ㅜㅠ - 훈다리 훈다리

[ㅇㄹ(rerereq)]

Z3도 별로 흥미없었는데 F*에 들어가니까 좀 흥미생김 너도 그걸 써먹을 플랫폼을 만들어야 흥미를 끌어올수 있을것

[기괴공학도(mecheng98)]

알겠음. 고마움. 그런데 구현할 수 있어야 말이지. - 훈다리 훈다리