commit f0739fc40c15d859f26f996e924deac756b4826b Author: coolguy Date: Sun Aug 30 00:35:48 2026 +0900 초기 커밋: thesis 문서와 OCaml v0 스캐폴딩 문서(docs/thesis.md)에 네 가지 파생 결정을 반영: - Effect 다형성: effect 변수는 타입 파라미터와 동일 규율(선언 명시, 해소는 호출 지점에서 로컬). 집합 의미론으로 row polymorphism 회피. - 인터페이스 경계: public 경계 전면 명시, 본문 추론 누출 금지, interface hash는 정규화된 시그니처 텍스트만으로 계산. - 모듈/패키지: content hash는 무결성이지 가용성이 아님을 명시. - 형식 명세 범위를 capability의 affine 규칙까지 확장. 스캐폴딩은 CLI 형태만 고정하고 파이프라인 단계는 비워 둔다. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..4e66100 --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +_build/ +*.install +.merlin diff --git a/.ocamlformat b/.ocamlformat new file mode 100644 index 0000000..93464b3 --- /dev/null +++ b/.ocamlformat @@ -0,0 +1,2 @@ +profile = default +version = 0.29.0 diff --git a/bin/dune b/bin/dune new file mode 100644 index 0000000..a8ab755 --- /dev/null +++ b/bin/dune @@ -0,0 +1,4 @@ +(executable + (name main) + (public_name cool) + (libraries coollang)) diff --git a/bin/main.ml b/bin/main.ml new file mode 100644 index 0000000..3f78185 --- /dev/null +++ b/bin/main.ml @@ -0,0 +1,34 @@ +let usage = + {|coollang toolchain + +사용법: + cool check ... 타입/effect/capability 검사 (fast path) + cool run typed IR 인터프리터로 실행 + cool version 버전 출력 +|} + +let report = function + | Ok () -> 0 + | Error errors -> + List.iter + (fun e -> prerr_endline (Coollang.Driver.string_of_error e)) + errors; + 1 + +let () = + let argv = Array.to_list Sys.argv in + let code = + match List.tl argv with + | "check" :: files -> report (Coollang.Driver.check files) + | [ "run"; file ] -> report (Coollang.Driver.run file) + | [ "version" ] -> + print_endline Coollang.Version.string; + 0 + | [] | [ "help" ] | [ "--help" ] | [ "-h" ] -> + print_string usage; + 0 + | cmd :: _ -> + Printf.eprintf "알 수 없는 명령: %s\n\n%s" cmd usage; + 2 + in + exit code diff --git a/docs/thesis.md b/docs/thesis.md new file mode 100644 index 0000000..bfc55f5 --- /dev/null +++ b/docs/thesis.md @@ -0,0 +1,125 @@ +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( + f: fn(a) -> b effects e, + xs: List + ) -> List 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 의미를 바꾸는가? / +기존 개념의 중복 표현인가? → 강한 이유 없으면 거절 diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..357e321 --- /dev/null +++ b/dune-project @@ -0,0 +1,10 @@ +(lang dune 3.24) + +(name coollang) + +(package + (name coollang) + (synopsis "coollang — a language optimized for time-to-trust") + (depends + (ocaml (>= 5.4)) + (dune (>= 3.24)))) diff --git a/lib/driver.ml b/lib/driver.ml new file mode 100644 index 0000000..1c73c79 --- /dev/null +++ b/lib/driver.ml @@ -0,0 +1,17 @@ +(* v0 파이프라인의 자리표시자. + parse -> name resolution -> type check -> effect/capability check + -> interface artifact + hash -> (cool run 시) 얇은 typed IR -> interpreter + + 각 단계는 별도 모듈로 분리해 들어온다. 지금은 CLI 형태만 고정한다. *) + +type error = { file : string; message : string } + +let string_of_error { file; message } = Printf.sprintf "%s: %s" file message + +let check (files : string list) : (unit, error list) result = + match files with + | [] -> Error [ { file = ""; message = "검사할 파일이 없습니다" } ] + | file :: _ -> Error [ { file; message = "check 파이프라인이 아직 구현되지 않았습니다" } ] + +let run (file : string) : (unit, error list) result = + Error [ { file; message = "interpreter가 아직 구현되지 않았습니다" } ] diff --git a/lib/dune b/lib/dune new file mode 100644 index 0000000..43cfe86 --- /dev/null +++ b/lib/dune @@ -0,0 +1,2 @@ +(library + (name coollang)) diff --git a/lib/version.ml b/lib/version.ml new file mode 100644 index 0000000..ffabb0c --- /dev/null +++ b/lib/version.ml @@ -0,0 +1 @@ +let string = "0.0.0-dev" diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..edfcadf --- /dev/null +++ b/test/dune @@ -0,0 +1,3 @@ +(test + (name test_coollang) + (libraries coollang)) diff --git a/test/test_coollang.ml b/test/test_coollang.ml new file mode 100644 index 0000000..c10ef2e --- /dev/null +++ b/test/test_coollang.ml @@ -0,0 +1,8 @@ +let () = assert (String.length Coollang.Version.string > 0) + +let () = + match Coollang.Driver.check [] with + | Error [ _ ] -> () + | _ -> failwith "빈 입력에는 오류가 나야 한다" + +let () = print_endline "ok"