주제 · 개념
정형 기법
증명, 검증, 명세로서의 타입. 특히 기계가 코드를 작성하게 된 이후에.
- 상위
- 프로그래밍 언어
- 페이지
- 4
지도에서 페이지 4개와 주변 주제
2026
- 13 분
The Proof You Only Have to Write Once
Generation is cheap, so verification is the bottleneck — and we throw the verification away every time. What if a proof, once written, could be named, shared, and vouched for? A content-addressed commons for verified Haskell, and the move I left for after the semantic-artifact trilogy.
- 7 분
The Field Exists Now
Alasdair Allan's agentlanguages.dev catalogue turns AI-oriented programming languages from a loose set of experiments into a field with camps, disagreements, and testable claims.
- 27 분
Source Code Is the New Assembly
Closing the trilogy. The artifact you author is no longer source code. It is a typed, verifiable object that carries meaning. Code becomes a lowering target.
- 26 분
The Last Programming Language Might Not Be for Humans
Three futures for programming languages as AI becomes the primary author of code, and why I bet on Haskell.