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( 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 전제가 스며들어 재작성 됨. 지금, 얇게. ※ 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 의미를 바꾸는가? / 기존 개념의 중복 표현인가? → 강한 이유 없으면 거절 ■ 측정 (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는 다시 볼 이유가 없다.