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 하나. 단순성의 기준은 "작성자"가 아니라 "리뷰어와 검증기"

■ 파생 결정

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<a>,
          f: fn(a) effects e -> b,
      ) effects e -> List<b>
  ※ 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 의미를 바꾸는가? /
기존 개념의 중복 표현인가? → 강한 이유 없으면 거절

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

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

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

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

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

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

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

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

■ 내장 테스트
test "이름" { ... }. 파라미터가 없으므로 capability를 받을 수 없고,
capability를 만드는 문법도 없다. 따라서 effect-free임이 증명된다 —
관례가 아니라 검사다. 그 결과:
- 파일도 시계도 못 건드린다. 같은 입력이면 같은 결과다
- 순서에 의존하지 않고 병렬로 돌려도 같다 → 결과를 캐시할 수 있다
  (인터페이스 해시가 안 변하면 재검사하지 않는 것과 같은 논리)
- 자원을 가질 수 없다 (획득에 effect가 필요하므로). 그래서 "테스트가
  죽으면 자원은?"이라는 질문이 애초에 생기지 않는다
interface hash에 들어가지 않는다 — 테스트를 고쳤다고 downstream이
재검사되면 안 된다.
컴파일 타임 메타프로그래밍 없음. assert는 std/test.cool에 coollang으로
쓰인다 (panic 위의 설탕) — 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는
다시 볼 이유가 없다.