bendlang/bend

Bend 2: a fast language that blocks AI mistakes via proof. Install: curl -fsSL https://bend-lang.com/install.sh | sh

Bend – 내장 증명을 갖춘 고속 병렬 언어

개요 – Bend는 고성능 컴파일러(CPU에서 C 수준, GPU에서 CUDA 수준의 속도 지향)와 증명 보조기 스타일의 타입 시스템을 결합한 오픈소스 프로그래밍 언어입니다. 이 언어를 사용하면 LAWS.bend라는 파일에 laws(형식 사양)를 작성할 수 있습니다. 컴파일러는 코드 변경 시 수학적 증명을 요구하여 해당 사양이 절대 깨지지 않음을 보장합니다. 이는 AI가 생성한 코드를 사람이 일일이 읽지 않아도 신뢰할 수 있도록 만드는 수단으로 자리 잡고 있습니다.

핵심 개념

고속 실행 – 강력한 정적 타입, 순수성, 선형성 덕분에 컴파일러는 수천 개의 GPU 코어로 확장되는 네이티브 C, Metal, CUDA 또는 JavaScript 코드를 생성하며, 이는 수동으로 작성한 코드만큼 빠릅니다.
고속 검증 – 동일한 컴파일러가 1초 이내에 증명을 검사합니다. 이는 Isabelle, Agda, Lean, Coq와 같은 기존 증명 보조기보다 훨씬 빠릅니다.
암시적 병렬 처리 – 명시적인 스레드나 잠금이 필요하지 않습니다. 런타임이 자동으로 순수 계산을 사용 가능한 모든 CPU/GPU 코어에 분할하고 결과를 결합합니다.
법칙 기반 개발 – LAWS.bend 파일은 불변 조건(예: “모든 잔액의 합은 0이어야 한다”)을 인코딩합니다. 코드가 수정되면 컴파일러는 불변 조건이 유지된다는 증명을 요구하여, 이를 위반하는 AI 생성 변경 사항을 차단합니다.

일반적인 워크플로우

LAWS.bend에 하나 이상의 법칙을 작성합니다.
LLM(또는 사람)에게 코드 구현이나 수정을 요청합니다.
bend PROOF.bend를 실행합니다. 컴파일러가 법칙에 따라 증명을 검사합니다.
증명이 성공하면 코드가 고속 실행 파일로 컴파일되고, 실패하면 변경 사항이 거부됩니다.

구문 예시(의존 타입이 있는 Python 스타일)

import Base

def main() -> IO(Unit):
  do IO<Unit>:
    name : String <- IO.try(String, IO.get_env("USER"))
    IO.print("Hello, " ++ name)

법칙과 그 증명:

law add_zero:
  for x: Nat
  {Nat.add(x, 0n) == x : Nat}

def add_zero(x):
  match x:
    case 0n: {==}
    case 1n+xp:
      %add_zero(xp) : {1n+Nat.add(xp, 0n) == 1n+_ : Nat}
      {==}

저장소의 주요 구성 요소

bend2/ – 컴파일러 및 표준 라이브러리 (base.bend).
paper/ – 타입 이론 (BendTT) 및 병렬 런타임 (BendRT)을 설명하는 학술 PDF.
bench/ – 성능 차트에 사용되는 벤치마크 프로그램.
tools/bend-fmt-lsp – 구문 전용 언어 서버 기능을 제공하는 포맷터/LSP.
demos/ – 각각 고유한 LAWS.bend를 가진 작은 예제 애플리케이션.

설치

curl -fsSL https://bend-lang.com/install.sh | sh

이 스크립트는 bend 명령줄 도구를 설치하며, 이를 통해 컴파일, bend guide 실행, 코드 포맷팅 등을 수행할 수 있습니다.

현재 제한 사항(README에 명시된 내용)

코드 장황함: 모든 것에 주석이 필요하며 타입 추론이 없음.
타입 클래스, 트레이트, 컴파일 타임 템플릿 외의 매크로가 없음.
증명 탐색/전술이 없음. 증명은 수동으로 작성해야 함.
아핀 값으로 인해 클로저/배열을 자유롭게 공유할 수 없음.
표준 라이브러리가 제한적임(TLS, HTTP, JSON, 정규식 등 없음).
단일 파일 프로그램만 가능. 증분 빌드 없음.
GPU 지원은 프로그램당 하나의 장치로 제한됨. 다중 머신 실행 없음.
Windows는 일급 타겟이 아님(WSL은 작동). JavaScript 타겟은 단일 스레드로 실행됨.
도구가 최소화됨: 포맷터 LSP만 있고 디버거, 프로파일러, REPL, 풍부한 진단 기능이 없음.
컴파일러 자체가 대부분 AI에 의해 생성되었으며 완전히 감사되지 않음.

커뮤니티 및 리소스

웹사이트: https://bend-lang.com
Discord, Twitter/X, Reddit, GitHub issues(지원 및 토론).
전체 언어 가이드 (GUIDE.md), 공식 Lean 모델 (bend.lean), 학술 논문(심층 이해).

결론 – Bend는 AI 시스템이 생성하는 검증 가능하고 고성능인 코드라는 새로운 요구를 충족하는, 실제적이고 활발하게 유지 관리되는 언어 프로젝트입니다. 아직 초기 단계라 많은 편의 기능이 부족하지만, 고속 실행 과 고속 증명 검사라는 핵심 약속은 시스템 프로그래밍, 형식 검증, AI 보조 개발의 교차점에서 주목할 만한 실험입니다.

bendlang/bend

Bend – 내장 증명을 갖춘 고속 병렬 언어

관련