Ada 언어를 SPARK와 함께 사용하는 것은 특히 안전성(Safety), 신뢰성(Reliability), 그리고 형식 검증(Formal Verification)이 중요한 학위 논문(특히 박사 논문) 주제에 대해 Rust보다 유리할 수 있는 강력한 이점을 제공합니다.

1. 🔍 형식 검증(Formal Verification)의 용이성

• SPARK 연계의 용이성: Ada 언어는 그 설계 철학상 SPARK라는 형식 검증 도구 및 언어 서브셋과 연계하기가 매우 쉽습니다.

  • SPARK는 Ada 언어의 서브셋으로, 수학적 방법을 사용하여 프로그램의 특정 영역에 버그가 없음을 증명할 수 있게 해줍니다. 이는 런타임 오류가 없음과 프로그램 사양과의 일치 여부를 증명하는 데 사용됩니다.

  • Rust 역시 Kani, Prusti, Verus와 같은 외부 도구를 통해 형식 검증을 지원하지만, Ada/SPARK는 언어 및 프로필 차원에서 계약(contracts), 동시성 규율, 타이밍 분석 등을 **일급 객체(first-class concerns)**로 취급하여 더 넓은 안전성 보장 범위를 제공합니다.

• 학위 논문에서의 이점:

  • 박사 논문과 같이 일반화된 개념을 도출하고 수학적 증명이 핵심인 연구에서는, 코드가 특정 속성(예: 범위 안전성, 논리적 계약 등)을 만족함을 자동화된 도구로 수학적으로 증명할 수 있다는 점이 매우 유리합니다.

    
    

2. 강력한 타입 시스템 및 안전성 확보

• 광범위한 안전성 정의: Rust가 주로 메모리 안전성과 데이터 경합 없음에 초점을 맞추고 이를 컴파일 타임에 보장하는 데 특화되어 있다면, Ada는 범위 서브타입(range subtypes), 판별자(discriminants) 등을 통해 **논리적 계약(Logical Contracts)**과 타입 안전성(Type Safety) 등 더 광범위한 안전성 문제를 언어 차원에서 다룹니다.

  • 예를 들어, Ada에서는 각도(Degrees)를 0부터 359까지만 허용하는 타입으로 정의하고 산술 연산을 모듈러(modular)로 설정하여 유효한 값 범위를 벗어나는 오류를 사전에 방지할 수 있습니다.

• 실시간/안전 필수 시스템: Ada와 SPARK는 항공전자, 철도, 국방과 같은 안전 필수 시스템(Safety-critical systems) 분야에서 오랜 기간 검증되고 사용되어 왔기 때문에, 해당 분야의 연구 주제에서는 Rust보다 필드 테스트와 적용 사례가 풍부하다는 장점도 있습니다.

  
  

3. ✍+ 가독성 및 기술(記述) 용이성

• 소스 코드의 기술 문서화: Ada는 Pascal과 유사한 장황한(verbose) 문법을 사용하며 begin ... end와 같이 명확한 블록 구조를 가집니다.

  • 이러한 특징 때문에 소스 코드 자체가 일종의 기술 문서처럼 기능하여, Ada 언어에 대한 지식이 부족한 사람도 코드를 쉽게 이해할 수 있습니다. 이는 논문에 알고리즘 구현의 명확성을 높이고 독자에게 코드를 설명하는 데 도움을 줄 수 있습니다.

Ada, Rust & the Future of Safe Code, with Quentin Ochem, EEI #54는 Ada, SPARK 및 Rust를 안전 필수 시스템의 맥락에서 비교하며 형식 방법 및 정적 분석의 역할을 다루고 있어 관련 정보를 얻는 데 도움이 될 수 있습니다.