Files

T

koriweb 5ba5a55c78 feat: Wiki 지식 자산 업데이트 - UX Scenarios, Frontend, Game Design, Topics 추가 [2026-05-08]

2026-05-08 19:52:07 +09:00

3.9 KiB

Raw Blame History

id, title, category, status, canonical_id, aliases, duplicate_of, source_trust_level, confidence_score, tags, raw_sources, last_reinforced, github_commit, inferred_by, tech_stack

title

CompCert-C-Compiler

📌 한 줄 통찰 (The Karpathy Summary)

"오류가 증명되지 않은 컴파일러: 소스 코드가 기계어로 번역되는 과정에서 컴파일러 자체의 버그로 인해 프로그램의 의미가 변질되지 않음을 수학적으로 완벽하게 증명한 세계 최초의 고신뢰성 C 컴파일러."

📖 구조화된 지식 (Synthesized Content)

CompCert는 Coq 증명 도우미를 사용하여 공식적으로 검증된 C 언어 컴파일러입니다. (Xavier Leroy 등이 개발)

핵심 가치:
- Formal Verification: 컴파일러의 모든 패스(Pass)가 원본 코드의 의미를 보존한다는 것을 수학적으로 정형화하여 증명.
- Bug-Free Compilation: 일반적인 컴파일러(GCC, Clang 등)에서 발견되는 '컴파일러 버그'로 인한 오작동 원천 차단.
- Safety-Critical Standard: 항공, 의료, 원자력 등 절대적 안전이 필요한 임베디드 시스템의 표준. (Reliability와 연결)
왜 중요한가?:
- 아무리 소프트웨어를 잘 짜도 컴파일러가 틀리면 소용없는데, CompCert는 신뢰의 사슬(Chain of Trust)에서 가장 중요한 고리를 수학으로 고정했기 때문임.

⚠️ 모순 및 업데이트 (Contradictions & Updates)

과거 데이터와의 충돌: 과거에는 정형 검증된 소프트웨어는 실성능 정책이 매우 떨어진다고 생각했으나, CompCert 정책은 최적화 정책(Optimization)을 적용하면서도 증명 정책을 유지하며 GCC 2단계 최적화 수준의 우수한 성능 정책을 보여주어 편견 정책을 깼음(RL Update).
정책 변화(RL Update): 이제는 단순 컴파일러를 넘어, 하드웨어 설계 정책이나 운영체제 정책(seL4 등) 전체를 정형 검증하려는 'Full-stack Verification 정책'의 선구자적 모델로 자리 잡음.

🔗 지식 연결 (Graph)

Reliability, Safety-Critical, Scientific-Method, Technical-Architecture, Formal-Verification
Key Tools: Coq proof assistant, Xavier Leroy.

🤖 LLM 활용 힌트 (How to Use This Knowledge)

언제 이 지식을 쓰는가:

(TODO)

언제 쓰면 안 되는가:

(TODO)

🧪 검증 상태 (Validation)

정보 상태: needs_review
출처 신뢰도: A
검토 이유: (P-Reinforce Phase 1 자동 정규화. 본문 검증 필요.)

🧬 중복 검사 (Duplicate Check)

기존 유사 문서: (TODO: 인덱서 클러스터 리포트 참조)
처리 방식: UPDATE (자동 정규화)
처리 이유: Phase 1 정규화 — 옛 템플릿/누락 필드 보강.

🕓 변경 이력 (Changelog)

날짜	변경 내용	처리 방식	신뢰도
2026-05-08	P-Reinforce Phase 1 정규화 (frontmatter + 헤더 표준화)	UPDATE	A

💻 코드 패턴 (Code Patterns)

패턴 1: (TODO: 이 프로젝트 컨벤션 반영한 구조 스켈레톤)

# TODO

🤔 의사결정 기준 (Decision Criteria)

선택 A를 써야 할 때:

(TODO)

선택 B를 써야 할 때:

(TODO)

기본값:

(TODO)

❌ 안티패턴 (Anti-Patterns)

[안티패턴]: (TODO: 무엇을 하면 안 되는가 + 이유 + 대신 무엇을)

3.9 KiB Raw Blame History