llm이 써 준 부록이다..

더 나은 예제가 있는지 찾아봐야겠어.

부록 B: 동일 안전성 목표 하의 코드 비교 - Rust vs. Ada/SPARK

이 부록은 본문 5장에서 철학적 차원으로 다룬 ‘의도 중심’과 ‘규칙 중심’의 설계 방식이, 실제 코드에서는 어떻게 구현되는지 구체적으로 비교 분석합니다.

이를 위해, ‘정수 오버플로 방지’라는 동일한 안전성 목표를 설정하고, 각 언어가 이 문제를 해결하는 접근 방식과 그 과정에서 개발자가 겪는 경험이 어떻게 다른지 독자 여러분께서 직접 판단하실 수 있도록 구성했습니다.

비교 과제: 32비트 정수 배열의 합계를 오버플로 없이 안전하게 계산하기

우리의 목표는 32비트 정수(i32)로 이루어진 배열의 합을 구하는 함수를 만드는 것입니다. 이 과정에서 합계가 32비트 정수의 최댓값을 넘어 발생하는 ‘정수 오버플로(Integer Overflow)’를 반드시 방지하거나, 안전하게 처리해야 합니다.

접근법 1: 러스트 (Rust) - ‘실패 관리’를 통한 안전성

러스트의 접근 방식은 연산이 실패할 수 있음을 인정하고, 그 실패 가능성을 타입 시스템으로 명시하여 호출자가 반드시 처리하도록 강제하는 것입니다.

// [src/main.rs]

// 오버플로가 발생하면 'None'을 반환하여, 실패를 명시적으로 알립니다.

fn checked_sum(slice: &[i32]) -> Option<i32> {

    let mut total: i32 = 0;

    for &item in slice {

        // total에 item을 더한 값이 i32의 범위를 넘으면 None을 반환하고 함수를 즉시 종료합니다.

        // 이것이 러스트 방식의 '실패 처리'입니다.

        total = total.checked_add(item)?;

    }

    Some(total)

}

fn main() {

    let numbers_ok = vec![1_000_000_000, 1_000_000_000];

    let numbers_overflow = vec![2_000_000_000, 2_000_000_000];

    // 성공 사례 처리

    if let Some(result) = checked_sum(&numbers_ok) {

        println!("[OK] The sum is: {}", result);

    } else {

        println!("[OK] The sum overflowed!");

    }

    // 실패 사례 처리

    if let Some(result) = checked_sum(&numbers_overflow) {

        println!("[Overflow] The sum is: {}", result);

    } else {

        println!("[Overflow] The sum overflowed!");

    }

}

실행 결과:

[OK] The sum is: 2000000000

[Overflow] The sum overflowed!

러스트 방식 분석

핵심 철학: 실패 관리(Failure Management). 오버플로는 발생할 수 있는 ‘실패’이며, Option<T> 타입을 통해 이 실패 가능성을 호출자에게 명확히 전달합니다.

개발자 사고 과정: 개발자는 “이 연산은 실패할 수 있으니, 실패를 알려주는 checked_add 함수를 써야겠다”고 생각합니다. 컴파일러는 ? 연산자와 Option 타입을 통해, 그 실패를 호출자가 if let 등으로 처리하도록 강제합니다.

어려움: 개발자는 러스트의 소유권 규칙과 Option/Result로 대표되는 에러 처리 패러다임에 익숙해져야 합니다. 즉, 컴파일러의 ‘규칙’에 적응하는 것이 주된 허들입니다.

안전성의 기본값: 릴리즈 모드에서는 성능을 위해 오버플로를 허용(wrapping)하는 것이 기본값입니다. 안전은 checked_add처럼 **‘선택(Opt-in)’**해야 합니다.

접근법 2: Ada/SPARK - ‘설계 기반 실패 방지’를 통한 안전성

Ada/SPARK의 접근 방식은 설계 단계에서부터 실패 가능성 자체를 원천적으로 제거하여, 런타임에 오류가 발생할 여지를 남기지 않는 것입니다.

-- [my_math.ads - 명세 파일]

package My_Math with SPARK_Mode is

   type Integer_Array is array (Integer range <>) of Integer;

   -- 합계가 32비트 정수(Integer) 범위를 넘을 수 있음을 '의도'하고

   -- 반환 타입을 64비트 정수인 Long_Long_Integer로 명시적으로 설계합니다.

   function Sum (Arr : Integer_Array) return Long_Long_Integer;

end My_Math;

-- [my_math.adb - 구현 파일]

package body My_Math with SPARK_Mode is

   function Sum (Arr : Integer_Array) return Long_Long_Integer is

      -- 계산 과정에서 오버플로가 발생하지 않도록

      -- 누적 변수(Total) 역시 64비트 정수 타입을 사용합니다.

      Total : Long_Long_Integer := 0;

   begin

      for I in Arr'Range loop

         Total := Total + Long_Long_Integer(Arr(I));

      end loop;

      return Total;

   end Sum;

end My_Math;

증명 결과: SPARK의 정적 분석 도구(GNATprove)는 이 코드를 분석한 후, 어떤 입력에 대해서도 런타임 오류(오버플로 포함)가 절대 발생하지 않음을 수학적으로 증명하고 “Proved” 메시지를 출력합니다.

Ada/SPARK 방식 분석

핵심 철학: 설계 기반 실패 방지(Failure Prevention by Design). 32비트 정수들의 합은 32비트를 넘을 수 있다는 사실을 인지하고, 64비트라는 더 큰 그릇을 준비하여 오버플로가 ‘물리적으로 불가능한’ 코드를 설계합니다.

개발자 사고 과정: 개발자는 “결괏값이 이 범위를 넘을 수 있으니, 더 큰 타입을 써야겠다”는 ‘의도’를 코드(타입 선언)로 직접 표현합니다. SPARK 도구는 개발자의 의도가 타당하며, 그 결과 런타임 오류가 발생하지 않음을 증명해주는 역할을 합니다.

어려움: 개발자는 코딩에 앞서 문제의 속성(값의 범위 등)을 먼저 분석하고, 그것을 해결할 수 있는 올바른 타입과 로직을 사전에 설계해야 합니다. 즉, 개발자의 ‘의도’를 명확히 정의하는 것이 주된 허들입니다.

안전성의 기본값: 일반적인 Ada 코드는 기본적으로 모든 연산에서 오버플로를 검사하는 ‘런타임 체크 코드’를 자동으로 삽입하고, 오류 발생 시 복구 가능한 예외(Constraint_Error)를 발생시킵니다. SPARK는 이 런타임 체크가 필요 없을 정도로 코드가 완벽함을 증명하여, 개발자가 안심하고 런타임 체크를 비활성화하여 최고의 성능을 얻을 수 있도록 보장하는 역할을 합니다.

결론: 두 방식의 비교