COOLLANG — 핵심 결정 요약

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

■ 언어 철학 (모든 결정의 뿌리)
1. 오류는 더 일찍: 컴파일 타임으로 최대한 끌어당김
   → null 없음(Option), Result, exhaustive matching, definite init,
     미선언 effect = compile error
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
4. 리뷰는 의미 단위로: 도구가 semantic diff 제공
   → "Effects: +payment.refund" 수준으로 리뷰 압축
5. 한 개념 = 한 방식: syntax variant 최소화, 공식 formatter 하나,
   공식 toolchain 하나. 단순성의 기준은 "작성자"가 아니라 "리뷰어와 검증기"

■ 파생 결정

동시성 (철학 1,2,3에서 파생):
- green thread (async/await의 function coloring은 철학 5 위반)
- structured concurrency만 허용: 태스크 수명 = 블록 구조 (locality)
- 데이터 경쟁은 격리로: mutable은 단일 소유, channel로 소유권 이동,
  공유는 immutable만 (borrow checker는 complexity budget 초과)
- spawn은 effect로 선언 → 동시성이 시그니처에 드러남

Effect 다형성 (철학 2,5에서 파생):
- effect 변수는 타입 파라미터와 정확히 같은 규율을 따른다:
  시그니처에 선언은 명시 강제, 해소는 호출 지점에서 로컬 unification
      fn map<a, b, e: effects>(
          f: fn(a) -> b effects e,
          xs: List<a>
      ) -> List<b> effects e
  ※ 전역 추론이 배제하는 것은 "선언 없이 프로그램 전체를 보고 알아내기"이지
     선언된 변수의 로컬 해소가 아니다. map 체크에 필요한 것은
     map과 인자의 시그니처뿐 (locality 유지)
- effect는 순서 없는 집합, 변수는 집합 변수, 합성은 합집합 → 결정 가능·로컬
- row polymorphism 불필요: 차집합("이 effect만 빼고")이 필요해지는 것은
  handler를 넣을 때이고, 그것은 v0 범위 밖
- 완화 장치 하나만 예약: 클로저 인자의 effects 생략 시 {}로 기본 해석
  (추론이 아니라 기본값이므로 헌법 위반 아님)

인터페이스 경계 (철학 2 + incremental + AI context locality가 한 점에서 만남):
- public 함수 경계에서 타입과 effect는 전부 명시
- 본문의 추론 결과는 어떤 것도 인터페이스로 새지 않는다
- interface hash는 명시된 시그니처 텍스트(정규화 후)만으로 계산한다
  ※ 본문 한 줄 수정이 해시를 흔들면 incremental 전제가 무너진다

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 + capability를 담는 자원의 affine 규칙
  ※ 주장은 두 정리의 결합이다 — (i) capability 없이는 effect를 수행할 수 없다,
     (ii) capability는 safe code에서 복제·위조되지 않는다.
     (ii)가 빠지면 핸들 복제 한 번으로 (i)이 공허해진다
  ※ 일반 데이터의 ownership 전체는 형식화 대상이 아니다.
     보안 주장을 지탱하는 non-duplication 성질만 증명 대상
- 명세와 구현을 같이 키우되 충돌 시 명세가 이긴다

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

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

포함 (되돌리기 비싼 것 전부):
- parse → name resolution → type check → effect/capability check
- interface artifact + hash 기반 incremental invalidation
- cool check
- 얇은 typed IR + tree-walking interpreter (cool run 대용)
  ※ IR을 미루면 non-IR 전제가 스며들어 재작성 됨. 지금, 얇게.
  ※ effect check가 fast path 예산 안에 드는지가 사활 → 최우선 검증 대상

제외 (아키텍처 검증 후 얹어도 되는 것):
- generics, contracts, 일반 ownership(자원 몇 개 하드코딩으로 대체)
- 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 탈출구(명시적 타입 하나)

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

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