제대로 디자인된 프로그래밍 언어의 쓰임새

이 광근

수정일 11/2011

프로그래밍 언어의 인기도는 분명 ``성적순''은 아니다. 현재 인기를 누리고 있는 언어들(C, C++, Java등)은 프로그래밍 언어 분야의 중요한 연구성과들을 충실히 구현한 언어들은 아니기 때문이다.

프로그램의 실행(evaluation), 기획(type), 프로그램 명시와 증명(spec and proof)등에 대해서 수학적으로 모델을 만들고 엄밀하게 찾아낸 해결방안들을 실제의 프로그래밍 언어로 최대한 담아낸 것들이 여럿 있음에도 불구하고 많은 사람들은 알고있지 못하거나 아직은 실용적이지 않을 것이라고 짐작하고 있다.

사실은, 중요한 소프트웨어의 개발에 이러한 튼튼한 기초를 가진 언어들이 그 장점을 살려 이용되고 있는 경향이 점점 빈번해지고있다. Phil Wadler는 이러한 언어가 실제 문제에 성공적으로 적용된 많은 예들을 정리해 놓고 있는데, 이들 내용과 그리고 꾸준히 증가하는 많은 예들을 정리해 본다.

소프트웨어 검증 시스템

서울대 프로그래밍 연구실에서 상용화한 Sparrow라고 하는 시스템이 OCaml로 구현되었다. Sparrow는 C/C++ 소스에 있는 메모리 오류 지점을 자동으로 검증해 주는 소프트웨어이다. 한 카피당 5만불에서 15만불의 가격으로 판매되고 있다.
MS사에서 판매하는 device driver 개발 kit에 있는 MS Window Vista drivers static verifiers는 OCaml로 구성되었다. 소프트웨어 검증기의 성능과 생산성이 OCaml 덕택이었슴을 그 홈페이지에서 밝히고 있다.
HP의 HP9000시리즈 서버와 다중프로세서 시스템의 버스 프로토콜이 HOL 증명기로 검증하는 과정을 통해서 오류를 발견하게 되었다. 이 오류는 몇달에 걸친 테스트과정에서 잡아낼 수 없었던 것이었다. 고차논리(higher-order logic) 증명기인 HOL은 Standard ML 이라는 함수형 언어로 짜여져 있다.
호주의 국방성 산하 연구원에서는 Isabelle이라는 증명기를 통해서 적기의 미사일을 유인하는 장치를 검증하였다. Isabelle도 Standard ML로 짜여져 있다.
HOL과 Isabelle 이외에, 여러개의 증명기(theorem prover)들이 개발되었는데, 대부분 함수형 언어로 구현되어있다: Coq는 ML의 프랑스 사투리인 Caml로, Veritas는 Miranda로, Yarrow는 Haskell로, 그리고 Alf, Elf, Lego등은 Standard ML로 구현되 있다.

컴파일러 시스템

상위의 타입구조를(higher-order and typed) 갖춘 언어들의 컴파일러들은 대부분 자기자신의 언어로 구현되어 있다:
- OCaml compiler system in OCaml
- Standard ML/NJ compiler system in SML
- nML compiler system in nML
- Haskell compiler system in Haskell
MIT의 Fast Fourier Transform Library (C programs) Compiler system인 FFTW가 OCaml로 작성되었다.

통신 시스템 소프트웨어

스웨덴의 Ericsson사에서 개발한 Mobility Server 는 12개국이상에 수출되서 사용되고 있는데, 그 스위칭 소프트웨어가 자체적으로 개발한 함수형 병렬언어인 Erlang 으로 구현되어있다(수십만 줄). 그 스위칭 시스템중에 하나가, Strasbourg에 위치한 전유럽 국회의사당 내의 핸드폰을 콘트롤하고 있다.
그 밖에도 Erlang으로 개발된 상용전화시스템 소프트웨어들은 AXD301 (Ericsson), GRPS (Ericsson), SSL accelerator (Nortel), ISD platform (Nortel) 등 계속증가추세에 있다.
Erlang시스템의 성공담에 대한 흥미있는 리뷰 슬라이드 (Erlang Workshop 2001, invited tutorial)

데이타베이스 시스템

AT&T와 Lucent Technologies사의 스위칭 소프트웨어에서 데이타 베이스의 자료를 검증하는 시스템 모듈이( Pdiff) Standard ML로 구성되어 있다(3만줄).
Human Genome 프로젝트에 필요한 데이타베이스 시스템의 질의어 요구조건이 미국의 에너지부에서 주관한 워크샵에서 공표된 적이 있는데(1993년), CPL/ Kleisli 시스템이 그 요구조건을 모두 만족시키는 질의어 처리 시스템으로 제안되었다. CPL은 함수형 언어이고, Kleisli는 Standard ML 로 구성된 시스템이다.

내장형 소프트웨어 시스템

프랑스 Dassault사에서 만드는 라팔 전투기나 소형 비지니스 젯트기등에 내장되는 많은 핵심 소프트웨어들이 Esterel Technologies라는 회사를 통해 Esterel이라는 synchronous programming language system의 기술로 제작되고 검증되고 있다.
미국 Raytheon사에서 제작하는 미사일추적/격추 시스템에 들어가는 디지탈 시그널 처리 과정의 "block convolution processing" 모듈이 Objective Caml을 이용해서 개발되고 있다.

분산처리 시스템

코넬대학에서의 분산 컴퓨터 환경에서 작동하는 groupware 시스템인 Ensemble이 Objective Caml이라는 ML의 사투리로 구현되있다.

애니매이션 라이브러리

Microsoft의 애니메이션 라이브러리인 Fran은 Haskell이라는 함수형 언어로 구현되었다.

그밖에도

Viaweb Store라는 인터넷 쇼핑몰 저작도구시스템이 Lisp으로 구성되어 있다. Viaweb Store는 Yahoo! Store를 포함한 14,000개 정도의 인터넷 쇼핑몰에 사용되었고, 이 분야 소프트웨어의 best seller이다.
왜 Lisp을 이용해서 그러한 소프트웨어를 제작하게 되었고, 그 결과 다른 경쟁회사보다 우위에 서게된 이유에 대한 글을 읽어보자.
Lufthansa 항공사의 승무원 스케쥴링 소프트웨어를 스웨덴의 Carlstedt Research and Technology사에서 Haskell로 구현하여 제공하였다.
HP의 ECDL 넷트웍 콘트롤 언어, Lolita 라는 자연어 처리 시스템등이 모두 함수형 언어를 이용해서 구현되었다.
파리의 Orly공항과 Roissy공항에 뜨고내리는 모든 비행기는 Ivanhoe라는 전문가 시스템에 의해 처리된 비행장 이용 서비스와 그 경비내역을 보고받는다. 이 시스템은 Haskell과 유사한 함수형 언어로 구현되있다.
MIPS2000/3000 simulator가 Standard ML로 구현되어 사용되고 있다.
프로그램의 유사성을 정량화하는 소프트웨어인 CloneChecker가 nML로 구현되었다.

국내에서도

서울대 프로그래밍 연구실에서 상용화한 Sparrow라고 하는 시스템이 OCaml로 구현되었다. Sparrow는 C/C++ 소스에 있는 메모리 오류 지점을 자동으로 검증해 주는 소프트웨어이다. 한 카피당 5만불에서 15만불의 가격으로 판매되고 있다.
Fasoo.com(주)의 Sparrow 사업팀에서도 OCaml를 주언어로 사용하고 있다.
서울대 프로그래밍 연구실에서 삼성전자를 위해 개발한 Airac(아이락, 愛樂) 분석기(C 프로그램의 배열 오류 검증기)가 nML 로 구축되어 있다.
KAIST 프로그램분석시스템 연구단에서 개발하는 nML 컴파일러 시스템이 nML자체로 구성되어있다
KAIST 프로그램분석시스템 연구단에서 개발하는 다양한 응용 프로그램들(Internet 전화시스템인 netPhone등)이 nML로 구성되어 있다.
LG 정보통신에서 제작하고 있는 PowerPC 기반의 스위칭 시스템 코드를 생성해내는 EM-to-PowerPC 컴파일러 시스템이 Standard ML로 구성되어 있다.
(주)듀오닉스 에서는, 타임시프트 기능과 네트워크 클라이언트/서버 기능을 가진 홈미디어 서버의 응용프로그램을 Ocaml을 사용하여 구현하고 있다.

제대로 디자인된 언어의 장점 /Standard ML /OCaml /nML /Scheme /Haskell