coollang/docs/thesis.md

COOLLANG — 핵심 결정 요약

■ 핵심 문제 (단 하나) AI의 코드 생성 속도 >> 신뢰 확보 속도. 병목은 생성이 아니라 검증. 언어는 "생성→신뢰"까지의 시간을 최소화한다.

■ 언어 철학 (모든 결정의 뿌리)

1. 오류는 더 일찍: 컴파일 타임으로 최대한 끌어당김 → null 없음(Option), Result, exhaustive matching, definite init, 미선언 effect = compile error ※ definite init은 문법이 이미 보장한다: let은 항상 초기화식을 요구하고 미초기화 바인딩을 쓸 방법이 없다. 별도 검사가 필요 없는 것이 맞다 ※ exhaustive matching은 interface hash가 enum 정의 본문을 입력으로 삼는 이유이기도 하다. upstream에 variant가 하나 늘면 downstream의 match가 깨져야 하는데, 이 검사가 없으면 깨질 것이 없다
2. 검증은 더 빨리: 검증 속도가 언어 설계의 헌법 → fast path(check) / slow path(release, deep verify) 분리 → 컴파일을 느리게/비결정적으로 만드는 기능 원천 배제 (전역 추론, 복잡한 trait solver, 임의 매크로, compile-time 유저 코드 실행) → locality: 함수 검증에 repo 전체 불필요. compiler locality = incremental locality = AI context locality → interface hash 동일 → downstream invalidation 없음
3. 피해는 더 좁게: 권한은 명시적 capability로만 전달 → ambient authority 없음. AI가 틀려도 언어가 폭발 반경 봉쇄 → 자원(File, Lock, Secret 등)은 affine ownership → affine은 전이된다: affine 필드를 가진 타입은 자동으로 affine
4. 리뷰는 의미 단위로: 도구가 semantic diff 제공 → "Effects: +payment.refund" 수준으로 리뷰 압축
5. 한 개념 = 한 방식: syntax variant 최소화, 공식 formatter 하나, 공식 toolchain 하나. 단순성의 기준은 "작성자"가 아니라 "리뷰어와 검증기"
6. 이름은 관례가 아니라 뜻에서 고른다 — 낯섦은 한 번 치르고 끝나지만 부정확함은 읽는 사람마다 매번 치른다 → 판정: 그 단어로 그것이 무엇인지 평범한 문장을 써 보라. 단어가 문장을 도우면 맞는 이름, 문장과 싸우면 틀린 이름이다 "크래시는 복구하는 것이 아니라 조사하는 것이다" — 돕는다 "패닉은 복구할 수 없다" — 다른 언어에서는 할 수 있어 싸운다 → 널리 쓰인다는 것은 옳다는 증거가 아니다. 운영체제의 "fault"가 그렇다 — 잘못이 아닌 것을 잘못이라 부르고, 그 오류까지 함께 전파된다 ※ 관례가 정확하면 관례를 따른다. 관례라서가 아니라 정확해서다 ※ 이름에만 적용된다. 동작을 관례와 다르게 만들 이유는 아니다

■ 파생 결정

Alias/Move 모델 (철학 1,3에서 파생 — 언어 전체의 토대): ※ 없는 것은 borrow checker와 lifetime이지 alias 규칙이 아니다. 최소 move 모델은 v0 필수다.

• 모든 타입은 copyable 또는 affine 둘 중 하나. 일반 데이터는 copyable, 자원·capability는 affine
• affine 값은 모든 경로에서 move다: 대입, 함수 인자, 반환, channel 전송, container 삽입, closure by-move capture. moved 이후 사용은 compile error ※ 이 검사는 함수 로컬 데이터플로우만으로 결정된다 (전역 분석 불필요)
• 분기 병합은 보수적 합집합: 한 분기에서라도 moved면 병합 지점 이후 moved ※ 블록당 O(변수 수)로 결정적이고, 오류는 "이 분기에서 move됨" 한 줄로 끝난다 ※ 경로별 정밀 추적은 정밀도를 사고 오류 설명 가능성을 파는 거래라 헌법과 역방향. "분기 간 불일치 = 에러"는 if c { consume(f) } else { consume(f) }까지 막아 과잉 ※ 조건부 소비가 반환으로 우회를 강요하는 것은 인정하는 대가다. 우회 자체가 "소비 여부를 타입에 드러내라"는 압력이라 리뷰 가능성에는 순기능이고, 실제로 고통스러우면 v1에서 Option::take류 표준 관용구로 흡수한다
• v0의 자원·capability는 affine이다: 중복 사용은 compile error, 미해제는 검사하지 않는다 (오용 금지, 누수 허용). linear 검사와 해제 보장은 v1 과제
• v0에 first-class reference는 없다. mutable 데이터는 소유 변수를 통해서만 변경
• 클로저는 mut 바인딩을 capture할 수 없다. 참조가 없으므로 별칭을 만들 수도, 조용히 복사할 수도 없기 때문이다. spawn 클로저 제한은 이 일반 규칙의 특수 사례다
• v0에 부분 move는 없다. 필드 접근은 빌림이고 결과도 빌린 값이다 ※ struct에서 affine 필드만 꺼내 가려면 부분 move 상태 추적이 필요한데, 그 복잡도는 v0가 사려는 것이 아니다. 필요하면 통째로 own으로 받는다
• 외부 타입은 affine임을 증명할 수 없으므로 copyable로 본다. 모르는 것을 위반이라고 말하지 않는다 — 모듈 로딩이 생기면 판정된다
• 공유는 deep immutable 값만 가능 (내부 가변성 타입은 v0에 없음) 근거: "safe code에 data race 없음"은 spawn만 막아서 성립하지 않는다. closure, channel, container, 인자/반환 전 경로에서 mutable alias가 없어야 하며, 값 의미론

• move-only가 이를 borrow 분석 없이 닫는 유일한 단순 모델이다. 대가: 값을 "빌려주고 돌려받는" 패턴은 반환으로 명시해야 한다. v1에서 제한적 second-class borrow로 완화 예정.

Capability 전달 (Alias/Move 모델의 제3의 규칙): ※ 매 호출 move는 실용성이 붕괴하고, 자유 참조는 non-duplication이 붕괴한다. capability는 second-class "use" 전달을 기본으로 한다.

• 기본은 use(호출 동안의 임시 접근): 호출자는 호출 후에도 계속 보유하고, 피호출자는 사용만 할 수 있다
• use로 받은 capability는 탈출 불가: 반환 금지, struct 저장 금지, channel 전송 금지
• use는 전염된다: use 값을 capture한 closure는 그 자체가 use 값이 되고, use 값은 use로 표시된 파라미터 위치로만 전달할 수 있다 ※ closure를 저장하는 sink는 일반 fn 파라미터를 요구하므로 use-closure를 넘길 수 없다 → compile error. 판정에 필요한 정보가 전부 시그니처에 있고 검사는 로컬 ※ capture 전면 금지는 with_retry(fn(){ pay.refund() }) 같은 정당한 패턴까지 죽이므로 기각. 별도의 nonescaping 개념을 만들지 않고 use의 전염으로 정의해 "한 개념 한 방식"을 지킨다 (Swift @noescape, second-class values의 검증된 경로)
• 소유권 이전이 필요할 때만 명시적 move
• 파라미터 위치는 전부 기본이 use(빌림)이고, 소유 이전만 own으로 유표기한다. capability든 callable이든 일반 affine 값이든 규칙은 하나다 ※ 무표기-흔함 / 유표기-위험은 이미 언어의 다른 곳에 있는 규칙이다 (effect 없는 함수가 무표기, effect 있는 쪽이 effects 유표기). 새 조항이 아니라 같은 원칙의 적용이다 ※ 반대로 두면 클로저를 저장하지 않는 고차 함수 — 즉 표준 라이브러리의 거의 전부 — 가 표기로 도배된다. 위험한 쪽(소유를 가져가는 쪽)에 표기가 가야 리뷰어의 눈이 그리로 간다 ※ capability를 별도 규칙으로 두지 않는 이유: capability의 존재는 이미 타입과 effects 절에 드러난다. 표기가 실어야 할 정보는 "소유가 옮겨가는가"뿐이다
• 파라미터 밖(반환 타입, struct 필드, channel 원소)은 use가 애초에 불가능한 위치이므로 무표기로 항상 owned 의미다
• capability가 셋 이상 필요하면 capability struct로 접는다 (표준 관용구): struct Deps { pay: PaymentGateway, log: Logger, db: Database } use deps: Deps로 받으면 affinity 전이와 use 규칙이 그대로 적용되므로 새 언어 기능 없이 시그니처가 접힌다 ※ capability 3개 이상은 대체로 응집도가 낮다는 설계 신호이기도 하다 근거: non-duplication은 "복제 금지"이지 "재사용 금지"가 아니다. use는 복제를 만들지 않으므로 보안 정리와 양립하고, 탈출 금지가 locality를 보존한다.

Affinity 전이 (보안 주장의 필수 전제):

• capability(또는 affine 타입)를 필드로 포함하는 타입은 자동으로 affine이다. 컴파일러가 타입 정의에서 유도하며 전이적으로 적용된다
• copyable 선언과 affine 필드의 공존은 compile error
• 타입의 affinity는 exported interface surface의 일부이며 interface hash에 포함된다
• 이 전이는 closure 환경에도 동일하게 적용된다 (callable affinity): v0의 callable은 두 종류다 — fn(...) copyable. copyable·immutable 환경만 capture 가능 affine fn(...) affine 값을 소유할 수 있고, 자신도 affine이라 move 규칙을 따름 affine 값을 capture한 closure의 타입은 자동으로 affine fn이 되며 fn 위치에 대입 불가. affinity는 callable 타입 표기의 일부로 공개 시그니처와 interface hash에 포함된다 ※ bound method와 partial application도 "환경을 보관하는 값"이므로 같은 규칙 ※ use-closure(위 Capability 전달)는 affinity와 직교하는 파라미터 위치 속성이다 근거: 이 규칙이 없으면 Box{pay}를 복사하거나 affine 값을 capture한 closure를 복사하는 것만으로 capability가 사실상 복제되어 non-duplication 정리가 깨진다.

동시성 (철학 1,2,3에서 파생 — Alias/Move 모델의 특수 사례):

• green thread (async/await의 function coloring은 철학 5 위반)
• structured concurrency만 허용: 태스크 수명 = 블록 구조 (locality)
• 데이터 경쟁은 격리로: mutable은 단일 소유, channel로 소유권 이동, 공유는 deep immutable만 (borrow checker는 complexity budget 초과)
• spawn closure는 by-move capture 또는 immutable capture만 허용 (Alias/Move 모델의 mut capture 금지가 그대로 적용된다)
• spawn은 primitive가 아니라 TaskScope capability의 메서드다. effect spawn은 아래 "정적/동적 층 분리"대로 그 타입에 묶인다 (PaymentGateway.refund와 동형)
• TaskScope는 use-only(second-class)라 블록 밖으로 탈출할 수 없다 — Capability 전달의 use 메커니즘을 그대로 재사용한다
• join/cancel은 handle 소비 관례가 아니라 scope 구문의 실행 의미로 강제한다: scope { ... } 블록 종료 시 런타임이 자식 전원을 join/cancel한다 ※ v0는 affine 미소비(누수)를 허용하므로 handle 기반 보장은 애초에 불가능하다. 실행 의미로 옮겨야 그 허점이 사라진다
• 루트 TaskScope는 main에 주입 → ambient authority 없이 권한 사슬이 main부터 닫힌다
• scope는 자식을 만들고 부모를 구문에 적는다: scope inner = outer { ... } ※ 부모를 적지 않으면 자식의 부모가 "가장 가까운 스코프"가 되는데, 그것이 정확히 ambient authority다. 권한 사슬이 main의 루트 TaskScope부터 끊기지 않고 이어지려면 모든 자식이 부모를 이름으로 지목해야 한다 ※ 중첩이 결정적이다. 안쪽 블록에서 바깥 스코프에 붙이는 것(수명이 다른 태스크를 의도적으로 부모에 붙이는 정당한 패턴)이 outer.spawn / inner.spawn으로 그냥 갈린다 ※ "어느 스코프에 붙는 태스크인가"가 리뷰어 눈에 보이는 것 자체가 이 언어가 파는 물건이다. 타이핑을 줄이려고 여기서 깎으면 팔 물건이 없어진다

Effect 다형성 (철학 2,5에서 파생):

• effect 변수는 타입 파라미터와 정확히 같은 규율을 따른다: 시그니처에 선언은 명시 강제, 해소는 호출 지점에서 로컬 unification fn map<a, b, e: effects>( xs: List, f: fn(a) effects e -> b, ) effects e -> List ※ effects 절은 파라미터 목록 뒤, 화살표 앞이다. 함수 선언과 함수 타입이 같은 어순을 쓴다. 반환 타입 뒤에 두면 중첩 함수 타입에서 어느 쪽 effects인지 구문만으로 갈리지 않는다 — 괄호로 떠넘기지 않고 어순으로 없앤다. 읽기 순서도 "입력과 권한 → 출력"이 되어 자연스럽다 ※ 전역 추론이 배제하는 것은 "선언 없이 프로그램 전체를 보고 알아내기"이지 선언된 변수의 로컬 해소가 아니다. map 체크에 필요한 것은 map과 인자의 시그니처뿐 (locality 유지)
• effect는 순서 없는 집합, 변수는 집합 변수, 합성은 합집합
• 합집합이 있는 이상 일반 unification이 아니다 (해가 유일하지 않다). v0는 해소를 pattern unification으로 제한해 유일성과 선형 비용을 산다: · effect 변수는 어떤 파라미터의 effect 자리에 "단독으로" 등장해야 한다(결정 위치) · 변수의 해는 그 결정 위치에서 읽어오기만 한다 · 합집합 식은 결과 위치에만 허용하며 절대 분해하지 않는다 · 합집합 식이 기대 타입과 대조되는 위치는 compile error + 명시적 인스턴스화 요구 ※ 이 제한은 검사기가 아니라 구문 수준에 새긴다: 파라미터 위치의 effect 절 프로덕션은 effects <변수> 또는 effects { 리터럴 집합 }만 허용하고, 합집합 프로덕션은 결과 위치 전용이다. "검사기가 거부"가 아니라 "그런 문장이 존재하지 않음"이 되므로 오류가 파서의 한 줄로 끝나고, 형식 명세에서 증명할 대상도 그만큼 줄어든다 ※ map·filter·fold류는 전부 이 형태에 들어간다. 역산이 필요한 시그니처(peel류)는 작성 자체가 거부된다 — 표현력을 팔아 결정성을 사는 거래이고, 이 언어에서는 항상 그 방향이 맞다
• row polymorphism 불필요: 차집합("이 effect만 빼고")이 필요해지는 것은 handler를 넣을 때이고, 그것은 v0 범위 밖
• 완화 장치 하나만 예약: 클로저 인자의 effects 생략 시 {}로 기본 해석 (추론이 아니라 기본값이므로 헌법 위반 아님)

Effect의 정적/동적 층 분리 (철학 2,4에서 파생):

• 정적 층(effect check)은 타입 수준까지만 다룬다: PaymentGateway.refund. capability 값의 identity는 unification에 등장하지 않는다 (결정성·단순성 확보)
• "어느 capability 값이 쓰였는가"는 동적/툴링 층의 몫: capability는 unforgeable 하므로 값 전달 경로 추적, audit id, semantic diff로 귀속한다
• 즉 폭발 반경의 상한은 타입이 정적으로 보장하고, 정확한 귀속은 동적 층이 담당한다

인터페이스 경계 (철학 2 + incremental + AI context locality가 한 점에서 만남):

• public 함수 경계에서 타입과 effect는 전부 명시
• 본문의 추론 결과는 어떤 것도 인터페이스로 새지 않는다 ※ 본문 한 줄 수정이 해시를 흔들면 incremental 전제가 무너진다

interface hash의 입력 = 모듈 exported surface 전체의 의미적 정규형:

• exported 함수 시그니처 (effect 포함)
• exported type 정의 본문 (struct 필드, enum variant — exhaustiveness에 직결)
• 타입의 affinity (copyable / affine)
• exported constant의 타입과 값
• capability/effect 선언
• reexport된 선언을 완전히 해소한 정의 본문 (목록이 아니다) ※ 키워드는 reexport 단독이다. export는 "처음 내보내기"와 "다시 내보내기"를 흐리는데 이 둘은 hash 규칙에서 의미가 다르므로 구문에서도 달라야 하고, use는 capability 전달 전용으로 보존한다 ※ A의 enum에 variant가 추가되면 B의 소스가 그대로여도 B의 hash가 변하고, C의 exhaustive match가 재검사된다. "의미적 정규형"을 구현 수준까지 내린 것 원칙: downstream 검사 결과에 영향을 줄 수 있는 모든 것을 포함한다. 의심스러우면 넣는다 — 과잉 포함의 비용은 재검사지만 누락의 비용은 잘못된 캐시라는 비대칭.

invalidation 전파 = 고정점 규칙 ("direct dependents로만 전파"가 아니다):

1. 변경된 모듈 자체를 재검사
2. 재검사 전후의 interface hash를 비교
3. 달라졌을 때만 그 모듈의 dependents를 큐에 추가
4. 큐가 빌 때까지(= hash가 안정되는 고정점까지) 1~3 반복 ※ 순서가 중요하다. dependents를 먼저 재검사하면 "본문만 수정 시 downstream 0건"이 성립하지 않는다 — hash 비교가 dependents 재검사보다 앞서야 한다

Generics (철학 2에서 파생):

• 기본 shared implementation, monomorphization은 명시적 요청 시만
• "compile speed by default, runtime specialization by request"

모듈/패키지 (철학 2,5에서 파생):

• registry-less, repository-addressed (domain 기반 namespace)
• commit/content hash lock → 재현 가능 빌드
• content hash가 주는 것은 무결성이지 가용성이 아니다: 가용성(도메인 만료·레포 삭제)은 선택적 proxy/mirror가 해법의 자리이고, 이름 선점·소유권 분쟁은 사회적 문제라 언어 차원의 해법이 없다 (투명성 로그는 위조를 막지 분쟁을 막지 못한다). 둘 다 v0 범위 밖

명세 (철학 3에서 파생):

• Go식 산문 명세 + conformance test suite
• 형식 명세는 보안 주장을 지탱하는 최소 단위에만 투자: effect + capability + affine 전이 규칙 + non-duplication 성질 ※ 주장은 두 정리의 결합이다 — (i) capability 없이는 effect를 수행할 수 없다, (ii) safe code에서 capability는 복제·위조되지 않는다. (ii)가 빠지면 핸들 복제 한 번으로 (i)이 공허해지고, (ii)에는 affinity 전이가 필수 전제다 (없으면 wrapper 복사로 우회된다) ※ 일반 데이터의 ownership 전체는 형식화 대상이 아니다. 보안 주장을 지탱하는 non-duplication 성질만 증명 대상 ※ v0 보안 정리의 범위는 non-duplication까지다. 자원 해제 보장은 주장하지 않는다 (v0는 affine이므로 누수는 합법). 정리의 범위를 넓히지 말고 정직하게 적는다
• 명세와 구현을 같이 키우되 충돌 시 명세가 이긴다

이름/확장자:

• coollang 단독 표기 (스탠퍼드 Cool과 구별, golang 방식 검색성 확보)
• .cool (충돌 제로, 확장자 생략은 toolchain이 허용)

표기 (철학 2,5에서 파생 — 문법 상세는 docs/grammar.ebnf):

• 제네릭 인자는 대괄호 하나로 통일: List[a], map[Int, String](xs, f) ※ <>는 식 위치에서 비교 연산자와 갈리지 않아 turbofish 같은 제2 표기를 부른다. 대괄호는 전위=리스트 리터럴 / 후위=인스턴스화로 위치가 결정하므로 LL(1)이고 표기가 하나로 끝난다. 대가로 인덱싱 연산자를 두지 않는다 (List.at을 쓴다) ※ effect 규칙이 "합집합 위치에서는 명시적 인스턴스화 요구"이므로 식 위치의 인스턴스화 문법은 반드시 존재해야 한다. 추론으로 회피할 수 없다
• 수식어 순서: 바인딩 수식어(own, mut)가 먼저, 타입 수식어(affine)가 뒤: own affine fn(...) effects e -> b
• 문 구분은 줄바꿈이다 (Go식 자동 삽입). 공식 formatter가 하나뿐이라 함정이 봉쇄된다
• 블록은 식이다. 마지막 식이 블록의 값이고 return은 조기 탈출 전용 ※ if와 match가 식이면 let x = if c { a } else { b }를 재대입 없이 쓸 수 있다. mutable 변수와 덮어쓰기가 줄면 move 검사가 그만큼 단순해진다 — 기준은 검증기다
• match 가드는 v0에 없다 ※ 가드가 붙는 순간 그 분기가 패턴 전체를 덮는다고 말할 수 없어 exhaustiveness가 흐려지고, SMT 없이는 보수적으로 _ 분기를 강요하게 된다. 철학 1의 대표 항목을 문법 편의와 바꾸지 않는다. 필요하면 분기 본문에서 if를 쓴다
• 타입 이름은 그 타입에 딸린 함수의 이름공간이다: String.len(s), File.close(f). 별도의 정적 메서드 문법을 두지 않는다
• ?는 Result 전용으로 하드코딩한다 (trait solver가 없으므로 일반화 경로가 없다) ※ 조기 탈출도 블록 종료이므로 scope의 join/cancel은 ? 경로에서도 실행된다 ※ v1에서 linear를 넣으면 ?의 조기 탈출 경로마다 해제가 필요해진다. 이것이 암묵 drop 문제와 만나는 지점이다 — linear 설계는 이 제약을 안고 시작한다

■ v0 — "기능의 서브셋, 아키텍처의 풀셋" 목표: 시스템 속성(빠른 검증 루프)은 측정으로만 증명된다. 성공 기준(숫자): 10만 줄 규모에서 함수 수정 시 check 50ms 이내. 측정 시나리오는 둘로 분리한다 — (a) 본문만 수정(implementation-only): downstream 재검사 0건 (b) 시그니처 수정(interface 변경): hash 고정점까지만 전파 성공 기준(체감): 표준 라이브러리급 코드 샘플을 이 규칙(명시 effect 변수 포함)으로 작성해 리뷰 가능성 확인. 시그니처가 effect 변수로 도배되면 설계 실패다. ※ 최우선 검증 대상은 성능만이 아니다 — "이 설계로 짠 일상 코드가 읽을 만한가"가 같은 등급의 관문이다.

포함 (되돌리기 비싼 것 전부):

• parse → name resolution → type check → effect/capability check ※ 각 단계는 그 단계가 소유한 성질만 판정한다. 예: affinity는 타입 동등성이 아니라 substructural 성질이므로 타입 검사가 아니라 move 검사가 소유한다. 단계가 서로의 결론을 앞지르면 진단이 엉뚱한 곳에서 난다 ※ 다만 effect 검사는 타입 검사와 같은 순회에서 돈다. effect 변수의 해소가 타입 변수와 같은 지점(호출 지점의 지역 unification)에서 일어나므로, 떼어내면 순회와 인스턴스화를 두 번 하게 된다. 소유는 나뉘되 순회는 하나다 ※ v0는 과잉 선언(선언했으나 수행하지 않는 effect)을 오류로 보지 않는다. 외부 모듈의 effect를 모르는 상태에서는 판정할 수 없기 때문이다. 모듈 로딩이 생기면 lint 대상이다
• move/affinity 검사, capability use 규칙, affinity 전이
• effect 변수 (effect 다형성)
• interface artifact + hash 기반 incremental invalidation
• coolc check
• 얇은 typed IR + tree-walking interpreter (coolc run) ※ IR을 미루면 non-IR 전제가 스며들어 재작성 됨. 지금, 얇게. ※ 실행 시점에도 권한의 출처는 런타임 하나다. main이 선언한 capability만 넘어가고, 소스에는 capability를 만드는 문법이 없다 — 보안 정리 (i)의 실행 시점 대응물. TaskScope의 뿌리도 같은 이유로 런타임이 준다. ※ v0의 scope 실행 의미는 순차다. 구조가 먼저고 병렬성은 그 위의 최적화다 — 순서가 반대면 취소와 전파를 나중에 끼워 넣게 된다. ※ effect check가 fast path 예산 안에 드는지가 사활 → 최우선 검증 대상

제외 (아키텍처 검증 후 얹어도 되는 것):

• generics, contracts
• borrow checker, lifetime, first-class reference, 내부 가변성 타입
• linear 검사(자원 해제 보장), 암묵적 drop
• second-class borrow의 일반화 (v1)
• LLVM/cranelift, release build, 독립 verifier, semantic diff
• Mutex 등 공유 mutable 탈출구 (필요가 증명되기 전 열지 않음)

구현: OCaml (컴파일러 = 트리 변환, OCaml 홈그라운드, 개발속도 1.5~2배) 타깃: 개발 머신 하나 (크로스 플랫폼은 v0 목표에 무기여) ※ v0는 버릴 수 있는 물건. 진짜 산출물 = 검증된 아키텍처 + 명세 + 테스트

■ v1 — 성능과 툴링

• Rust 재작성 (salsa: 증분 프레임워크, cranelift/LLVM: backend) ※ 명세+테스트가 있으면 번역이지 재설계 아님 (rustc도 OCaml→self-hosting)
• cool build --release (LLVM), cool verify --deep (SMT 등)
• 독립 verifier: compiler를 통짜로 신뢰하지 않고 IR invariants 재검증
• semantic diff, IR 기반 semantic operations (AI 툴링)
• generics 완성, contracts, 공유 mutable 탈출구(명시적 타입 하나)
• named effect set (effects Checkout = {PaymentGateway.charge, Database.write}). v0는 풀어쓴다 — 무엇을 접어도 되는지는 리뷰 가능성 데이터가 쌓인 뒤에 안다
• 단일 스코프 함수 한정 scope 축약형 (체감 불만이 실제로 쌓였을 때만)
• 제한적 second-class borrow (Alias/Move 모델의 "반환으로 돌려받기" 대가 완화)
• linear 검사(자원 해제 보장). 사전 베팅: 암묵적 drop보다 명시적 close(f) 강제 + 미소비 시 compile error(순수 linear) 쪽이 coollang 철학에 맞는다 — effect가 코드에 보이는 자리가 생기고, "한 개념 한 방식"이 유지되며, AI가 생성한 코드의 해제 누락이 컴파일 타임에 잡힌다. defer/scope 문법 설탕은 그 위에 얹는다 ※ 암묵적 drop을 택하면 선언되지 않은 effect가 실행되어 철학 1과 정면 충돌한다. "drop이 effect를 일으키는 문제"를 함께 풀지 않고 linear만 얹을 수 없다

■ 검증 계층 (fast/slow 분리의 구체화) L0 parse / L1 type·effect·capability·ownership → 매번, ms 단위 L2 빠른 테스트 / L3 fuzzing / L4 formal proof → 요청 시, 분리 실행

■ 기능 추가 관문 (요약) 오류를 더 빨리 잡는가? / 컴파일 복잡도·시간은 예측 가능한가? / invalidation 범위를 넓히는가? / unrelated code 의미를 바꾸는가? / 기존 개념의 중복 표현인가? → 강한 이유 없으면 거절

■ 실패의 세 층 — 실패 / 결함 / 감독 서로 다른 세 질문에 답한다. 아래 층은 위 층 없이도 성립한다.

실패 (Result) 호출자가 대처할 수 있는가? 타입이 강제한다 결함 (crash) 이 태스크가 계속할 수 있는가? 컴파일러는 추적하지 않는다 감독 죽은 태스크를 어떻게 다루는가? capability가 강제한다

세 층이 세 가지 다른 기제로 규율된다는 것이 제대로 나뉘었다는 증거다. "상황이 나쁨"은 결함이 아니라 실패다 — 디스크가 가득 찬 것은 Result다. 이 선을 긋지 않으면 crash가 게으름의 배출구가 된다. ※ 취소는 이 셋 중 어디에도 없다. 취소는 실패가 아니라 "더 이상 필요 없음" 이며 별도의 결정으로 남는다. "오류"는 컴파일러가 내는 진단에만 쓴다.

■ 결함 — crash crash(message) -> Never. 키워드다 (prelude가 없어 함수로 두면 매번 import).

• effect가 아니다. 경계 검사 하나에 {Crash}가 호출자 전부로 전염되면 effect 절은 신호가 아니라 잡음이 된다. 발산이 effect가 아닌 것과 같은 이유다 — 무한 루프도 추적하지 않는다.
• Never는 어떤 타입 자리에도 놓인다. 그래야 match 팔에서 쓸 수 있고, 그게 없으면 crash는 식 자리에서 못 쓴다.
• 언어 수준 recover가 없다. 붙잡는 것이 있으면 그것은 예외이고, 예외는 시그니처에 안 적히므로 철학 1과 충돌한다.
• 되감기를 하지 않는다. ※ crash 시 자원 해제 여부는 자원 모델과 함께 결정한다 — 지금은 열어둔다.
• 0으로 나누기, assert 실패, 미래의 범위·오버플로가 전부 이 하나로 모인다. ※ crash는 프로그램의 결함을 말한다. 예상되는 실패는 Result다. 호출자가 대처할 수 있는 것을 crash로 처리하면 오용이다.

■ crash는 어디까지 올라가는가 (실패의 단위) 콜 스택의 root가 아니라 scope 트리의 root다. 즉 실패의 단위는 프로세스가 아니라 태스크다. scope가 이미 그 모양이기 때문이다 — 렉시컬이고, 블록을 나가는 것이 join이며, 자식이 죽었다는 사실이 부모에게 도달하는 지점이 문법에 이미 있다(닫는 중괄호).

crash는 scope 트리를 타고 올라간다. 자식이 crash하면 그 scope는 join 지점에서 crash한다. root까지 도달하면 실행이 끝난다.

v0는 태스크가 하나뿐이라 이 규칙이 관측되지 않는다 — "태스크가 죽는다"와 "프로그램이 죽는다"가 같은 사건이다. 그래도 지금 적는 이유는, 동시성이 진짜가 될 때 이 결정을 새로 하면 이미 쓰인 코드의 의미가 바뀌기 때문이다.

전파는 취소를 정하지 않고도 정의된다. 취소가 생기면 형제들이 언제 멈추는지가 바뀔 뿐, scope가 실패한다는 사실은 바뀌지 않는다. ※ 형제 취소는 여전히 미정이다. 대가를 알고 미룬다 — 취소가 없으면 형제 하나가 끝나지 않을 때 죽은 자식의 crash가 join에 도달하지 못한다. 실패가 hang에 가려진다. 이것이 취소가 필요한 이유이기도 하다.

■ 얼랭 방식은 되는가 — 감독은 되고 비구조적 spawn은 안 된다 공유 가변 상태 없음, let it crash, 죽은 쪽의 상태를 물려받지 않음 — 얼랭과 이미 같다. 다른 경로로 같은 결론에 도착했다. 가져오지 않는 것: 얼랭의 비구조적 spawn(Pid가 부모보다 오래 산다). 부모 없는 태스크는 ambient authority와 같은 문제이고, 구조적 동시성을 고른 이유가 그것이다. 가져오는 것: 감독. scope 트리가 이미 supervision 트리 모양이다. sc.spawn(f) 실패가 부모로 전파된다 sup.spawn(sc, f) 실패가 여기서 멈춘다 spawn은 하나의 개념이고 실패가 어디까지 가느냐가 권한으로 갈린다 — 실패를 삼키려면 Supervisor를 받았어야 하고 그것이 시그니처에 보인다. 문법 변경 없음. 재시작 가능한 자식은 copyable 클로저여야 한다(fn vs affine fn). 얼랭이 관례로 지키는 것을 affinity가 이미 검사한다. 재시작 전략은 라이브러리다(얼랭도 OTP). ※ 전제조건은 자원 모델이다. 죽은 태스크가 잡았던 것이 정리되지 않으면 재시작이 곧 누수다. ※ 얼랭의 보장은 BEAM의 선점 스케줄링과 프로세스별 힙 위에 선다. 우리에겐 아직 둘 다 없다 — 이것은 설계 층의 답이지 v0가 보여줄 수 있는 것이 아니다.

■ 격리 경계는 recover가 아니다 런타임은 격리 경계를 가질 수 있다. 테스트 러너가 첫 사례이고, 서버의 요청 경계가 두 번째가 될 것이다. 구분선은 이것이다:

실패한 계산이 만든 값은 경계를 넘지 못한다. 경계가 얻는 것은 "죽었다"는 사실과 메시지뿐이다.

recover는 같은 스택에서 재개하고 지역 변수에 접근한다 — 금지다. 격리 경계는 죽었음을 관찰할 뿐이다 — 허용이다. Erlang의 supervisor가 죽은 프로세스의 상태를 물려받지 않는 것과 같다. 테스트 러너가 이 원칙대로다: 실패한 테스트에서 아무 값도 가져오지 않고 이름과 메시지만 얻는다. 서버 경계도 언어 기능이 아니라 scope 위에 얹는다.

■ 내장 테스트 test "이름" { ... }. 파라미터가 없으므로 capability를 받을 수 없고, capability를 만드는 문법도 없다. 따라서 effect-free임이 증명된다 — 관례가 아니라 검사다. 그 결과:

• 파일도 시계도 못 건드린다. 같은 입력이면 같은 결과다
• 순서에 의존하지 않고 병렬로 돌려도 같다 → 결과를 캐시할 수 있다 (인터페이스 해시가 안 변하면 재검사하지 않는 것과 같은 논리)
• 자원을 가질 수 없다 (획득에 effect가 필요하므로). 그래서 "테스트가 죽으면 자원은?"이라는 질문이 애초에 생기지 않는다 interface hash에 들어가지 않는다 — 테스트를 고쳤다고 downstream이 재검사되면 안 된다. 컴파일 타임 메타프로그래밍 없음. assert는 std/test.cool에 coollang으로 쓰인다 (crash 위의 설탕) — std에서 본문이 있는 첫 함수다. 실패 메시지에 값이 안 나오는 것은 의도다. 표현식 텍스트를 잡으려면 매크로가 필요하다. ※ effect 있는 코드는 테스트할 수 없다. 가짜 capability를 만드는 수단이 없기 때문이다. 실제로 불편해진 뒤에 판단한다.

■ lint (오류다, 경고가 아니다)

• 미사용 import: 쓰지 않는 모듈의 시그니처가 바뀌면 이 모듈이 재검사된다. 증분 루프의 비용을 이유 없이 넓히는 선언은 남겨둘 수 없다.
• effect 과잉 선언: 선언하고 수행하지 않으면 호출자가 하지도 않는 일에 의무를 진다. 시그니처는 실제보다 좁아도 안 되고 넓어도 안 된다. 단, effect 변수가 있거나 본문에 모르는 이름이 있으면 판정하지 않는다 — 무엇이 묶일지는 호출 지점이 정하고, 외부 타입의 메서드는 effect를 모른다. lint는 blocking이 아니다. 이름 해소 실패는 뒤 단계를 막지만 lint는 막지 않는다 — lint 하나가 진짜 타입 오류를 가리면 루프가 느려진다.

■ 파서 오류 복구 항목 단위로만 회복한다. 오류가 난 선언은 통째로 버리고 다음 선언에서 다시 시작한다. 문 단위로 더 잘게 회복하려 하면 파서가 추측을 하게 되고, 틀린 추측은 없는 오류를 지어낸다. 한 항목에 오류 하나가 상한이라는 것은 정직한 한계이지 숨길 것이 아니다. 동기화 지점: 중괄호 깊이 0 + 줄 첫머리 + 선언 시작 토큰. 셋 다 필요하다.

■ 표준 라이브러리 (std/) 본문 없는 선언 파일이다. 런타임이 구현하고 .cool 파일은 계약만 말한다. 구현이 아니라 시험대인 것이 요점 — effect 다형성이 실제로 쓸 만한지가 List.each와 List.map에서 결정된다. 규칙이 틀렸으면 여기서 드러난다. prelude는 없다. std도 명시적으로 가져온다 — 암묵적으로 끌어오지 않는다는 규칙에 예외를 두지 않는다. ※ std를 넣자마자 샘플 01이 깨졌다. List.each에 Result를 반환하는 클로저를 넘기고 그 안에서 ?를 쓰고 있었다. 검사되지 않던 코드가 검사되기 시작한 것이고, 이것이 std를 "부채 상환"이 아니라 "검증"으로 본 이유다. 결과를 버릴 방법이 언어에 없다는 성질도 여기서 처음 확인됐다.

■ 개밥 먹기 (2026-08) samples/app — 설정 파서 + 리포트 도구, 2모듈 232줄. 검사기를 시험하려고 쓴 것이 아니라 일을 하려고 쓴 첫 프로그램이다. 결과: 되돌리기 비싼 결정은 하나도 후회되지 않았고(capability 전달, effect 명시, 실패를 버릴 수 없음, 소진적 match), 불편은 전부 되돌리기 싼 것들이었다 — 리스트 n번째 접근 없음, String.concat 2항. "else if가 없다"고 적은 항목 하나는 확인해 보니 관찰자가 틀린 것이었다 — 개밥 먹기의 불편은 언어의 성질일 수도, 쓴 사람의 습관일 수도 있다. 전문과 증거는 docs/friction.md. 이것이 v1 설계의 첫 입력이다. 후속: std 보강(List.first/nth/enumerate, String.join, Option/Result 함수)으로 292줄이 232줄이 됐다. 문법은 하나도 건드리지 않았다 — 걸린 것이 전부 std의 빈 곳이었지 문법의 문제가 아니었다는 뜻이고, 그것 자체가 결과다. 마찰 8건 중 2건은 "언어가 못 한다"고 적었다가 확인해 보니 되는 것이었다 (else if, enumerate). 개밥 먹기에는 확인 절차가 함께 있어야 한다.

■ 측정 (2026-08, v0 fast path) 100,391줄 / 200 모듈 (사슬 의존). bench/bench.ml로 재현. cold 전체 검사 245ms 본문만 수정 0.8ms, 재검사 1개 모듈 시그니처 수정 2.1ms, 재검사 2개 모듈 (+ downstream 소진성 위반 검출) 증분 루프의 비용은 시간이 아니라 재검사 범위가 결정한다. 본문 수정이 downstream을 한 칸도 건드리지 않는 것이 이 아키텍처의 주장이고, 위 수치의 "재검사 1개"가 그 주장이다. 시그니처 수정이 사슬 끝까지 가지 않고 2개에서 멈추는 것도 같은 규칙의 결과다 — m101의 interface는 변하지 않으므로 m102는 다시 볼 이유가 없다.