▲devjeonghwan 3달전 | parent | ★ favorite | on: 타입은 어떻게 증명이 되는가 — TypeScript 타입 시스템과 Curry–Howard 대응(evan-moon.github.io)린팅이 아니라고 이야기는 하지만.. 타입 검사가 엄격한 Contract 이행임을 증명하려면, 그 계약이 바이너리와 런타임에서 강제되어야 하지 않을까요? 그렇지 않다면 그것은 여전히 floating한 구문 상태의 타입 린팅이 아닐까 싶습니다.
린팅이 아니라고 이야기는 하지만.. 타입 검사가 엄격한 Contract 이행임을 증명하려면, 그 계약이 바이너리와 런타임에서 강제되어야 하지 않을까요? 그렇지 않다면 그것은 여전히 floating한 구문 상태의 타입 린팅이 아닐까 싶습니다.