jordanhubbard/nanolang

해결하는 문제

NanoLang은 기계(예: LLM)가 작성하고 인간이 읽을 수 있도록 설계된 프로그래밍 언어와 안전한 런타임입니다. AI 에이전트가 코드를 생성할 때 오류를 유발할 수 있는 프로그래밍 언어의 모호성 문제를 해결합니다. 또한 커스텀 커널 없이 표준 커널에서 서비스를 호스팅할 수 있는 안전하고 최소 권한 환경을 제공합니다.

작동 방식

NanoLang은 모호하지 않은 구문과 Coq에서 형식적으로 증명된 핵심 의미론(타입 안정성, 진행성, 결정성 포함)을 사용합니다. 네이티브 성능을 위해 C로 트랜스파일할 수 있으며, 스택 기반의 가상머신인 NanoISA VM을 통해 실행할 수도 있습니다. NanoISA VM은 위험한 외부 호출을 별도 프로세스에서 격리하여 메인 프로그램에 영향을 주지 않도록 안정성을 보장합니다.

대상 사용자

기계 생성 코드용으로 형식적 검증된 안전한 언어가 필요한 개발자, 형식적 검증, 안전한 런타임, AI 기반 개발의 교차점에 관심 있는 사람들에게 적합합니다.

주요 특징

• 형식적 검증된 의미론: 공리나 인정된 하위 케이스 없이 Coq에서 기계적으로 증명된 핵심 의미론.
• NanoISA VM: FFI 호출을 코프로세스에서 격리하여 메인 프로그램에 영향을 주지 않도록 보장하는 검증된 바이트코드 VM.
• 기계 주도 최적화: 상수 접기, 죽은 코드 제거, 프로파일 기반 인라인화를 지원합니다.
• 안전한 런타임: 위조 불가능한 기능, POSIX 서비스 패브릭, 안전한 서비스 호스팅을 위한 트랩 저널을 제공합니다.
• 섀도 테스트: 함수 정의와 함께 필수적인 테스트 블록으로, 코드가 설계 단계부터 테스트되도록 보장합니다.
• LLM 호환: 기계가 읽을 수 있는 공식 사양(spec.json)과 학습용 참조(MEMORY.md)를 포함하여 LLM이 언어를 올바르게 작성할 수 있도록 지원합니다.