Rust vs Ada: 논리 버그 방지 관점에서

많은 개발자들이 Rust를 “버그 없는 언어”라고 생각합니다. 사실 Rust는 메모리 안전성과 동시성 안전성을 언어 차원에서 강력히 보장합니다.

• 소유권(ownership)과 빌림(borrowing) 규칙 덕분에 use-after-free, double free 같은 메모리 버그는 원천 차단됩니다.
• Option, Result 타입을 통해 null 포인터나 unchecked 예외도 줄어듭니다.

하지만 Rust는 **논리 버그(logical bug)**까지 자동으로 막아주지는 않습니다.
예를 들어, 배열 인덱스가 항상 유효해야 한다는 조건은 Rust에서 언어 차원에서 강제되지 않습니다. 개발자가 직접 타입 설계나 테스트로 확인해야 합니다.

Ada의 접근: 계약 기반 프로그래밍

Ada는 **계약 기반 프로그래밍(Contract-Based Programming)**을 지원합니다.

• 사전조건(Precondition): 함수가 호출되기 전에 만족해야 하는 조건
• 사후조건(Postcondition): 함수가 종료된 후 반드시 만족해야 하는 조건
• 불변식(Invariant): 데이터 구조가 항상 만족해야 하는 조건

이 계약들은 실행 시 검사될 수도 있고, SPARK Ada 도구(GNATprove 등)를 통해 정적 검증을 수행해 수학적으로 증명할 수도 있습니다. 즉, 논리 버그를 사전에 차단할 수 있습니다.

코드 예제 비교

🔹 Rust 예제 (논리 버그는 개발자가 직접 책임져야 함)

fn get_element(arr: &[i32], index: usize) -> i32 {
    // 논리 버그: index가 arr.len() 이상이면 panic 발생
    arr[index]
}

fn main() {
    let data = vec![10, 20, 30];
    println!("{}", get_element(&data, 5)); // 런타임에서 panic
}

Rust는 메모리 접근 오류를 막지만, index < arr.len()이라는 논리 조건은 언어 차원에서 강제되지 않습니다.

🔹 Ada 예제 (계약으로 논리 버그 방지)

with Ada.Text_IO; use Ada.Text_IO;

procedure Array_Access is
   type Int_Array is array (Positive range <>) of Integer;

   function Get_Element (Arr : Int_Array; Index : Positive) return Integer
      with Pre  => Index in Arr'Range,               -- 사전조건: Index는 배열 범위 내
           Post => Get_Element'Result = Arr(Index);  -- 사후조건: 반환값은 해당 원소
   is
   begin
      return Arr(Index);
   end Get_Element;

   Data : Int_Array := (1 => 10, 2 => 20, 3 => 30);

begin
   Put_Line(Integer'Image(Get_Element(Data, 2))); -- 정상 동작
   Put_Line(Integer'Image(Get_Element(Data, 5))); -- 검증 단계에서 오류 검출
end Array_Access;

Ada는 Index in Arr'Range라는 사전조건을 통해 배열 범위를 벗어난 접근을 원천적으로 차단합니다. GNATprove 같은 도구를 사용하면 이 조건을 정적으로 증명할 수 있어, 런타임에 도달하기도 전에 버그가 발견됩니다.

🚀 결론

• Rust: 메모리 안전성과 동시성 안전성은 탁월하지만, 논리 버그는 개발자가 직접 책임져야 한다.
• Ada: 계약 기반 프로그래밍을 통해 논리 조건까지 언어 차원에서 강제할 수 있으며, 정적 검증 도구로 수학적으로 증명 가능하다.

👉 따라서 배열 인덱스 범위, 상태 불변식, 알고리즘 조건 같은 논리 버그는 Ada가 더 강하게 방지할 수 있다. Rust는 범용 시스템 프로그래밍에 강력하지만, 논리적 안전성까지 언어 차원에서 보장하지는 않는다.