Ada 소개

Ada 소개 (Introduction)

Ada는 1980년대 초 미국 국방부가 주도해 만든, 고신뢰성(high-reliability)을 최우선으로 설계된 프로그래밍 언어예요. 임베디드·안전 필수 시스템에서 특히 강한 면모를 보여주는 언어로, 이 과정에서는 Ada 2012를 기준으로 언어의 핵심 개념을 하나씩 살펴봐요.

출처: Ada 소개 문서

본문

역사 (History)

1970년대 미국 국방부(DOD)는 프로젝트마다 서로 다른 비표준 방언이나 부분집합·초집합을 쓰는 바람에 프로그래밍 언어의 수가 폭발적으로 늘어나는 문제를 겪었어요. 그래서 공통의 현대적인 프로그래밍 언어를 요구하는 제안 요청서(RFP)를 내고, 그 승자는 CII Honeywell-Bull의 Jean Ichbiah가 제출한 안이었죠.

첫 번째 Ada 표준은 1983년에 발표됐고, 이후 1995년, 2005년, 2012년에 개정·강화되면서 유용한 새 기능들이 더해졌어요. 이 튜토리얼은 언어의 여러 버전을 나눠 가르치기보다 Ada 2012 전체를 하나로 다룰 거예요.

오늘날의 Ada (Ada today)

오늘날 Ada는 임베디드 실시간 시스템에서 많이 쓰이며, 그중 상당수는 안전 필수(safety-critical) 시스템이에요. Ada는 범용 언어로도 쓸 수 있지만, 정말 빛을 발하는 곳은 저수준 애플리케이션이에요:

  • 메모리 요구량이 낮은 임베디드 시스템(가비지 컬렉터 불가)
  • 하드웨어와의 직접 인터페이싱
  • 소프트/하드 실시간 시스템
  • 저수준 시스템 프로그래밍

Ada가 두드러지게 쓰이는 분야로는 항공우주·국방, 민간 항공, 철도 등이 있어요. 이런 애플리케이션은 높은 수준의 안전을 요구해요. 소프트웨어 결함이 단순한 불편이 아니라 심각한 결과를 초래할 수 있기 때문이죠. Ada는 결함을 이른 단계 — 대개 컴파일 시점이나 정적 분석 도구로 — 감지해주는 안전 기능을 제공해요. Ada는 또 다음과 같은 다양한 영역의 애플리케이션을 만드는 데도 쓸 수 있어요:

이것은 완전한 목록이 아니라, Ada가 어떤 종류의 프로그래밍에 적합한지를 보여주는 참고일 뿐이에요.

현대 언어 중에서 목표물과 추상화 수준이 가장 가까운 것은 아마 C++과 Rust일 거예요.

철학 (Philosophy)

Ada의 철학은 대부분의 다른 언어와 달라요. Ada 설계의 바탕에는 다음 원칙들이 있어요:

  • 가독성이 간결성보다 중요하다. 구문적으로 보면 기호보다 키워드를 선호하고, 어떤 키워드도 축약어가 아니라는 점에서 드러나요.
  • 매우 강한 타입 시스템. Ada에서는 새 타입을 도입하기 쉬워서 데이터 사용 오류를 막아주는 이점이 있어요. 많은 함수형 언어와 비슷하지만, Ada에서는 거의 타입 추론이 없어 프로그래머가 타입을 훨씬 명시적으로 지정해야 한다는 차이가 있죠.
  • 암묵적인 것보다 명시적인 것이 낫다. 이건 Python의 계명이지만, Ada는 우리가 아는 어떤 언어보다 훨씬 더 나아가요. 구조적 타입(structural typing)이 대부분 없고, 대부분의 타입은 프로그래머가 명시적으로 이름을 붙여야 해요. 앞서 말했듯이 타입 추론도 대부분 없어요.
  • 의미가 매우 잘 정의되어 있고, 미정의 동작(undefined behavior)이 절대 최소로 제한된다.
  • 프로그래머는 자신의 프로그램이 무엇을 뜻하는지에 대해 컴파일러(와 다른 프로그래머)에게 많은 정보를 줄 수 있어요. 그래서 컴파일러가 프로그래머에게 매우 도움(엄격함)이 될 수 있게 해요.

이 과정에서는 그런 철학을 이루는 개별 언어 기능들을 하나씩 설명할 거예요.

SPARK

이 수업은 Ada 언어 하나만 다루지만, Ada와 매우 가깝고 상호 운용 가능한 또 다른 언어가 있다는 점을 언급할 가치가 있어요 — 바로 SPARK 언어예요.

SPARK는 Ada의 부분집합으로, SPARK로 작성된 코드가 자동 증명(automatic proof)에 적합해지도록 설계됐어요. 이것은 일반적인 프로그래밍 언어보다 훨씬 높은 수준으로 코드의 정확성에 대한 보증을 제공해요.

SPARK 언어 전용 과정이 따로 있어요. 다만 이 과정에서 Ada의 명세 능력에 대해 말할 때마다, 그 힘은 SPARK에서 런타임 오류의 부재에서부터 형식적으로 명세된 기능 요구사항 준수에 이르기까지 프로그램 속성을 증명하는 데 활용할 수 있다는 점을 기억해두세요.

더 알아보기 (Learn more)

  • Ada 표준·역사 전반은 AdaCore 학습 포털에서 더 깊이 탐구할 수 있어요.
  • SPARK 언어의 자동 증명 기반 프로그래밍은 SPARK 과정에서 다뤄요.