coollang/docs/thesis.md

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
   → 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 데이터는 소유 변수를 통해서만 변경
- 공유는 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 전송 금지, 호출보다 오래 사는 closure에 capture 금지
  ※ 탈출 검사는 함수 로컬로 결정 가능
- 소유권 이전이 필요할 때만 명시적 move
근거: non-duplication은 "복제 금지"이지 "재사용 금지"가 아니다. use는 복제를
만들지 않으므로 보안 정리와 양립하고, 탈출 금지가 locality를 보존한다.

Affinity 전이 (보안 주장의 필수 전제):
- capability(또는 affine 타입)를 필드로 포함하는 타입은 자동으로 affine이다.
  컴파일러가 타입 정의에서 유도하며 전이적으로 적용된다
- copyable 선언과 affine 필드의 공존은 compile error
- 타입의 affinity는 exported interface surface의 일부이며 interface hash에 포함된다
근거: 이 규칙이 없으면 Box{pay}를 복사하는 것만으로 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만 허용.
  mutable 참조 capture는 문법적으로 금지
- 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 생략 시 {}로 기본 해석
  (추론이 아니라 기본값이므로 헌법 위반 아님)

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 선언
- re-export 목록
원칙: downstream 검사 결과에 영향을 줄 수 있는 모든 것을 포함한다. 의심스러우면
넣는다 — 과잉 포함의 비용은 재검사지만 누락의 비용은 잘못된 캐시라는 비대칭.

invalidation 전파 = 고정점 규칙 ("direct dependents로만 전파"가 아니다):
1. 변경된 모듈의 direct dependents를 재검사
2. 그중 interface hash가 실제로 바뀐 모듈만 다음 단계로 전파
3. hash가 안정되는 지점에서 중단
※ implementation-only 변경은 1단계에서 멈춘다 (hash 불변 → 전파 0)

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이 허용)

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

포함 (되돌리기 비싼 것 전부):
- parse → name resolution → type check → effect/capability check
- move/affinity 검사, capability use 규칙, affinity 전이
- effect 변수 (effect 다형성)
- interface artifact + hash 기반 incremental invalidation
- cool check
- 얇은 typed IR + tree-walking interpreter (cool run 대용)
  ※ IR을 미루면 non-IR 전제가 스며들어 재작성 됨. 지금, 얇게.
  ※ 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 탈출구(명시적 타입 하나)
- 제한적 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 의미를 바꾸는가? /
기존 개념의 중복 표현인가? → 강한 이유 없으면 거절