From 994e2362adac2d79f83e7260366f2f3e57231d40 Mon Sep 17 00:00:00 2001 From: coolguy Date: Sun, 30 Aug 2026 00:44:08 +0900 Subject: [PATCH] =?UTF-8?q?thesis:=20move=20join=20=EA=B7=9C=EC=B9=99=20?= =?UTF-8?q?=ED=99=95=EC=A0=95=EA=B3=BC=20affine/linear=20=EA=B2=BD?= =?UTF-8?q?=EA=B3=84=20=EB=AA=85=EC=8B=9C?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 두 미해결 항목을 닫는다. join 규칙 — 보수적 합집합으로 확정. 한 분기에서라도 moved면 병합 지점 이후 moved. 블록당 O(변수 수)로 결정적이고 오류가 한 줄로 끝난다. 경로별 정밀 추적은 오류 설명 가능성을 파는 거래라 채택하지 않고, "분기 간 불일치 = 에러"는 정당한 코드까지 막아 과잉이다. 조건부 소비의 우회 강요는 인정하는 대가이며, 필요하면 v1에서 관용구로 흡수한다. affine/linear — v0는 affine이다: 오용 금지, 누수 미검사. 따라서 v0 보안 정리의 범위는 non-duplication까지이며 자원 해제는 주장하지 않는다. linear 검사와 해제 보장은 v1 과제로 미루되, 암묵적 drop은 선언되지 않은 effect를 실행해 철학 1과 충돌하므로 명시적 소비 강제 방향을 사전 베팅으로 남긴다. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E --- docs/thesis.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/docs/thesis.md b/docs/thesis.md index 9281f41..9aa13bb 100644 --- a/docs/thesis.md +++ b/docs/thesis.md @@ -34,6 +34,16 @@ Alias/Move 모델 (철학 1,3에서 파생 — 언어 전체의 토대): - 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, @@ -137,6 +147,8 @@ Generics (철학 2에서 파생): (ii)에는 affinity 전이가 필수 전제다 (없으면 wrapper 복사로 우회된다) ※ 일반 데이터의 ownership 전체는 형식화 대상이 아니다. 보안 주장을 지탱하는 non-duplication 성질만 증명 대상 + ※ v0 보안 정리의 범위는 non-duplication까지다. 자원 해제 보장은 주장하지 않는다 + (v0는 affine이므로 누수는 합법). 정리의 범위를 넓히지 말고 정직하게 적는다 - 명세와 구현을 같이 키우되 충돌 시 명세가 이긴다 이름/확장자: @@ -167,6 +179,7 @@ Generics (철학 2에서 파생): 제외 (아키텍처 검증 후 얹어도 되는 것): - generics, contracts - borrow checker, lifetime, first-class reference, 내부 가변성 타입 +- linear 검사(자원 해제 보장), 암묵적 drop - second-class borrow의 일반화 (v1) - LLVM/cranelift, release build, 독립 verifier, semantic diff - Mutex 등 공유 mutable 탈출구 (필요가 증명되기 전 열지 않음) @@ -183,6 +196,12 @@ Generics (철학 2에서 파생): - 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 단위