Bosque
Bosque는 프로그램의 동작을 기계적으로 이해·검사하고 신뢰성 높은 소프트웨어를 만들기 쉽도록 설계된 프로그래밍 언어다. Microsoft Research에서 Mark Marron의 연구로 2019년 공개되었으며, 이후 독립된 BosqueLanguage 공개 소스 프로젝트로 발전했다....
| 분류 | 프로그래밍 언어, 정형 검증 지향 언어 |
|---|---|
| 최초 공개 | 2019년 |
| 초기 개발 | Microsoft Research |
| 후속 개발 | BosqueLanguage 공개 소스 프로젝트 |
| 설계 방향 | 규칙적인 의미론, 자동 분석 |
| 패러다임 | 함수형 의미론, 명령형 블록 문법 |
| 타입 체계 | 정적 타입, 대수적 자료형 |
| 주요 기술 | SMT 기반 분석, 타입 검사, 조건 검증 |
| 언어 구성 | 불변 값과 명시적인 상태 변화 |
| 컴파일 체계 | 중간 표현·C++ 변환 등 |
| 연구 분야 | 신뢰성, 프로그램 분석, AI 보조 개발 |
| 소스 모델 | 공개 소스 |
| 공식 프로젝트 | BosqueLanguage |
Bosque는 프로그램의 동작을 기계적으로 이해·검사하고 신뢰성 높은 소프트웨어를 만들기 쉽도록 설계된 프로그래밍 언어다. Microsoft Research에서 Mark Marron의 연구로 2019년 공개되었으며, 이후 독립된 BosqueLanguage 공개 소스 프로젝트로 발전했다. 일반적인 명령형 언어에 익숙한 개발자가 사용할 수 있는 블록·대입 중심 문법과 함수형 프로그래밍의 의미론을 조합하고, 언어와 컴파일러·분석 도구가 처음부터 함께 설계되는 방식을 강조한다.[1]
Bosque는 언어에 내재한 예외적인 동작과 해석의 불규칙성을 줄여 프로그램의 의미를 더 정확하게 분석할 수 있도록 하는 설계를 추구한다. 불변 값과 명시적인 상태 변경, 타입으로 구분되는 문자열·값, 사전·사후 조건과 불변식 등의 개념을 활용해 프로그램이 기대하는 조건을 코드의 구조에 드러내려 한다. 이와 같은 언어 구성은 코드에 대한 정적 분석과 테스트·검증을 자동화하기 위한 전제다.
컴파일러와 중간 표현(IR)은 Bosque의 핵심 연구 대상이다. 소스 코드를 분석하기 적합한 구조로 바꾸고 SMT 솔버가 처리할 수 있는 논리식으로 변환하여 특정 입력에서 오류가 발생하는지 검사하거나 조건의 성립 여부를 검증할 수 있도록 한다. 또한 C++ 코드 출력과 실행 환경 연구도 이루어지고 있다. 이렇게 언어의 의미론과 도구의 분석 능력을 함께 설계하는 접근은 사후에 정적 분석기를 추가하는 일반적인 언어 개발 방식과 구별된다.[2]
Bosque는 2023년 Microsoft의 초기 저장소가 보관된 뒤 개발 조직이 독립 프로젝트로 이동했으며, 새로운 버전과 컴파일러를 계속 발전시켰다. 최근의 개발 방향은 프로그램의 자동 검증뿐 아니라 API의 의미 정의와 AI 보조 개발에서 분석 가능한 코드를 제공하는 데 초점을 맞춘다. Bosque의 연구적 가치는 일반적인 표현력 외에 코드를 실행하기 전후로 기계가 프로그램의 성질을 얼마나 정확하게 파악하고 증명할 수 있는지 언어 차원에서 다룬다는 점에 있다.[3]