함수형 언어가 우주로 갔다고요? OCaml 위성 프로젝트 'Borealis' 이야기

여러분, OCaml이라는 언어 들어보셨나요? 대학교 컴파일러 수업이나 프로그래밍 언어 이론 책에서 한 번쯤 본 적은 있을 거예요. 함수형 프로그래밍 언어인데, 학계나 일부 마니아 커뮤니티에서 주로 쓰이는 좀 "고상한" 언어라는 인상이 강하거든요. 그런데 그 OCaml이 진짜 우주로 갔습니다. Borealis라는 위성 프로젝트인데, 위성에 탑재되는 펌웨어와 미션 소프트웨어 상당 부분을 OCaml로 짰다고 해요.

이게 왜 신기한 일이냐면, 우주에서 돌아가는 소프트웨어는 보수성의 끝판왕이거든요. NASA나 ESA(유럽우주국)는 보통 C, Ada, 그리고 정형 검증이 가능한 SPARK 같은 언어를 씁니다. 한 번 발사하면 고치러 갈 수가 없으니까 안정성이 최우선이고, 그래서 수십 년 동안 검증된 언어만 골라 쓰는 게 관행이에요. 그 와중에 OCaml처럼 가비지 컬렉터(GC, 메모리를 자동으로 정리해주는 기능)가 있는 언어를 들고 간다는 건 꽤 도전적인 선택이죠.

왜 하필 OCaml이었을까

저자가 꼽는 가장 큰 이유는 OCaml의 강력한 타입 시스템이에요. 타입 시스템이라는 게 뭐냐면, 컴파일러가 "이 함수는 정수만 받아야 해", "여기서 null이 들어오면 안 돼" 같은 규칙을 미리 검사해주는 장치예요. C로 짜면 런타임에 터지는 버그들이 OCaml에서는 컴파일 단계에서 거의 다 잡힙니다. 우주에서는 한 번 죽으면 끝이니까, 이런 정적 검사가 굉장히 값지죠.

또 하나는 패턴 매칭과 대수적 데이터 타입(ADT)이에요. 위성이 받는 명령은 종류가 정해져 있는데, OCaml로 쓰면 "이 명령은 이런 변형들만 가능해"라고 타입으로 못박을 수 있어요. 처리 안 된 케이스가 있으면 컴파일러가 친절하게 알려주죠. C로 짜다가 switch 문에 default 빼먹어서 미지의 상태로 들어가는 비극을 피할 수 있다는 거예요. 미션 크리티컬한 상태 머신을 짤 때 이게 얼마나 든든한지는 한 번이라도 비슷한 코드 짜본 분은 공감하실 겁니다.

GC 문제는 어떻게 해결했냐고요? OCaml의 GC는 비교적 예측 가능한 편이고, 위성 소프트웨어의 핫 패스(자주 실행되는 부분)에서는 메모리 할당을 최소화하는 방식으로 짠다고 해요. 필요하면 unboxed 표현이나 직접 메모리 관리도 가능하고요. 결국 "GC 있는 언어는 임베디드에 못 쓴다"는 통념이 슬슬 깨지고 있는 거예요.

우주 임베디드 언어의 흐름

흥미로운 건 OCaml만 이런 시도를 하는 게 아니라는 점이에요. Rust도 NASA JPL의 일부 프로젝트에 슬금슬금 들어가고 있고, 유럽 쪽 소형 위성 회사들도 Rust를 평가 중이거든요. 전통적으로는 Ada/SPARK가 우주의 왕이었는데, 모던 언어들이 도전장을 내미는 모양새예요.

함수형 언어 중에는 Haskell도 임베디드 영역 진입을 시도 중이고, 자율비행 시스템에서는 Lustre나 Esterel 같은 동기식 함수형 언어가 이미 쓰입니다. 에어버스 비행 제어 소프트웨어가 SCADE라는 비슷한 도구로 만들어진다는 사실, 알고 계셨나요? "비행기와 위성은 신뢰성 때문에 함수형으로 짠다"는 게 이제 농담이 아니에요.

한국 개발자에겐 어떤 의미가 있을까

당장 우리가 OCaml을 배워서 누리호에 코드를 올릴 일은 없을지 모릅니다. 하지만 이 사건이 시사하는 바는 분명해요. 타입 시스템과 정적 분석의 가치가 가장 보수적인 분야에서까지 입증되고 있다는 거예요. 한국에서도 토스, 카카오, 라인 같은 곳에서 TypeScript, Kotlin, Rust처럼 타입 안전한 언어로 적극 이전하는 흐름이 있잖아요. 단순 유행이 아니라 결함 비용이 높은 영역에서는 진짜로 효과가 있다는 얘기입니다.

또 한국항공우주연구원이나 KAIST 인공위성연구소 같은 곳에서 큐브샛(소형 위성) 개발이 활발한데, 주니어 개발자가 참여할 기회도 점점 늘고 있어요. 이런 분야에 관심 있다면 함수형 사고와 정형 검증에 대한 공부가 차별점이 될 수 있습니다. ReScript나 ReasonML로 OCaml의 문법을 슬쩍 맛보는 것도 좋고, 학습용으로는 "Real World OCaml"이라는 무료 책이 잘 정리돼 있어요.