bend

Bend 2는 AGI 이후 시대를 위해 설계된 새로운 프로그래밍 언어로, 인간이 AI 시스템에 모호함 없는 언어로 의도를 전달하는 것을 목표로 합니다. 핵심 혁신은 LAWS.bend로, 개발자가 불변식(법칙)을 선언하면 AI가 코드 변경 시 이를 수학적으로 증명해야 하며, 이를 위반하는 버그의 병합을 수학적으로 불가능하게 만듭니다. README에 명시된 주요 기능: **성능**: CPU에서 C 수준, GPU에서 CUDA 수준의 속도를 목표로 합니다. 벤치마크는 경쟁력 있는 단일 코어 성능과 수천 개 코어에 걸친 대규모 병렬 확장을 보여줍니다. 컴파일러는 강한 타입, 순수성, 선형성을 활용하여 최적화합니다. **증명 검사**: Isabelle, Agda, Lean, Coq보다 수십 배 빠른 검증을 주장하며, 복잡한 증명을 1초 미만으로 확인합니다. **암시적 병렬성**: 스레드, 잠금, 커널을 작성할 필요가 없습니다. 분할 정복 함수는 자동으로 모든 사용 가능한 CPU/GPU 코어에 분산됩니다. 예시로 pow2(20)이 4,096개의 GPU 코어에 분산됩니다. **AI 협업 워크플로우**: AI 지원 개발을 위해 설계되었습니다. 개발자는 LAWS.bend에 법칙(예: "잔액 합계는 0이어야 함", "플레이어는 벽을 통과할 수 없음")을 작성하고, 커밋 전에 AI가 `bend PROOF.bend`를 실행하도록 요구합니다. 컴파일러는 증명을 기계적으로 강제합니다. **언어 기능**: Python 유사 문법에 의존 타입을 갖습니다. 아핀/선형 타입 시스템(값 공유 불가)을 사용합니다. 종료 재귀가 필요하며(@unsafe 탈출구 제공), C, Metal, CUDA, JavaScript를 타겟으로 합니다. 기본 라이브러리는 최소이며, 효과로는 I/O, 채널, TCP/UDP, 파일 접근이 있습니다. **현재 제한 사항(명시적으로 나열됨)**: 장황한 주석, 타입 클래스/트레이트/매크로 없음, 전술이나 증명 탐색 없음, 제한된 숫자 타입(Nat, U32, F32만), 느린 문자열(연결 리스트), HTTP/JSON/TLS/정규식 없음, 프로그램당 단일 GPU, 증분 컴파일 없음, 느린 네이티브 컴파일, 최소한의 도구(LSP, 디버거, 포매터, REPL 없음), 컴파일러가 대부분 AI로 작성되어 감사되지 않음. 프로젝트에는 Lean 형식화(bend.lean), 학술 논문(BendTT 타입 이론, BendRT 런타임), 그리고 증가하는 데모 컬렉션이 포함됩니다. 커뮤니티 채널: Discord, Reddit, X/Twitter. 제공된 자료에는 라이선스가 명시되지 않았습니다.