세 줄 요약:1. Ada/SPARK는 어렵지 않으면서 러스트보다 더 높은 안전성, 신뢰성을 제공하는데,2. Rust는 타 언어 대비 매우 어려우면서 Ada보다 더 낮은 안전성, 신뢰성을 제공함.3. 따라서 이는 Rust 언어 설계 결함으로 바라보는 것이 적합함.


Ada/SPACK는 러스트보다 더 높은 안전성과 신뢰성을 제공하는데,예전에 c/c++/java 개발하던 직관적이고 익숙한 패러다임으로 개발하면 됨.
그러나 러스트의 경우 개발자 사람이 아닌, 컴파일러 입장으로 개발 패러다임을 변경해아 함.또한 러스트 언어 스펙이 고정되지 않아 사람 및 기계가 러스트 언어를 이해하거나 생성하기 어려움그래서 러스트가 어렵게 느껴지는 것.
이는 즉, 러스트 언어 설계 결함에 기인함.


3.4 비교 분석 2: Ada/SPARK의 수학적 증명과 보증 수준


본 절에서는 Ada 및 그 부분집합인 SPARK를 ‘분석적 도구’로 활용하여, 러스트의 안전성 모델이 시스템 프로그래밍의 안전성 보증 스펙트럼에서 어느 지점에 위치하는지를 기술합니다. SPARK의 ‘수학적으로 증명된 정확성’과 비교 분석을 통해, 러스트 모델의 공학적 특징과 보증 범위를 탐색합니다. 이 비교는 각기 다른 설계 철학이 선택한 상충 관계를 이해하기 위함입니다.


러스트의 안전성 보증: ‘정의되지 않은 동작(UB)’ 방지


3.2절에서 분석했듯이, 러스트의 핵심적인 안전성 보증은 ‘소유권’과 ‘빌림’ 규칙을 통해, 컴파일 시점에 정의되지 않은 동작(Undefined Behavior, UB)을 유발하는 메모리 접근 오류 및 데이터 경쟁(data race)을 방지하는 것입니다.

그러나 이 보증은 프로그램의 논리적 정확성(logical correctness)이나, 모든 종류의 런타임 오류(runtime error) 부재를 보증하지는 않습니다. 예를 들어 정수 오버플로, 배열 인덱스 초과 등의 오류는 panic(3.2.3절)으로 이어지며, 이는 시스템의 안정적 ‘실행’ 보장과는 구별됩니다.


Ada/SPARK의 안전성 보증: ‘프로그램 정확성’ 증명


반면, Ada/SPARK 생태계는 더 넓은 범위의 정확성을 목표로 합니다.

  1. Ada의 기본 안전성 및 회복력: Ada는 언어 차원에서 타입 시스템과 ‘계약 기반 설계(Design by Contract)’를 통해 논리적 오류 방지를 시도하며, 정수 오버플로를 포함한 런타임 오류 발생 시 예외(exception)를 발생시키는 것을 기본으로 합니다. 이는 오류 처리 루틴을 통해 시스템이 임무를 지속하게 하는 ‘회복력(resilience)’을 지향하는 설계입니다.

  2. SPARK의 수학적 증명: Ada의 부분집합인 SPARK는 정형 검증(formal verification) 도구를 통해 코드의 논리적 속성을 수학적으로 분석합니다. 이를 통해 런타임 오류(정수 오버플로, 배열 인덱스 초과 등 포함)가 발생하지 않음을 컴파일 시점에 ‘증명’할 수 있습니다.


오류 처리 설계의 차이: 복구(recover)와 중단(panic)


이러한 기술적 차이는 오류를 다루는 설계 철학에서 기인합니다.


  • Ada: 런타임 오류를 ‘예외’로 취급하여 시스템 복구(recover)를 지원합니다. 이는 오류가 발생하더라도 시스템 전체가 멈추지 않고 가용한 상태를 유지해야 하는 ‘미션 크리티컬(가용성 중시)’ 시스템의 요구사항을 반영합니다.
  • Rust: 동일한 오류를 프로그램의 ‘버그’로 취급하여 해당 실행 흐름을 중단(panic)시킵니다. 이는 잘못된 상태로 실행을 지속하여 발생할 수 있는 2차적인 문제(메모리 오염 등)를 방지하기 위해 ‘메모리 안전(무결성 중시)’을 우선시하는 설계입니다.


이 차이는 기능의 유무를 넘어, 각 언어가 목표로 하는 시스템의 성격에 따른 설계 목표의 차이를 나타냅니다.


두 언어의 보증 수준 비교


오류 유형 Rust Ada (기본) SPARK
메모리 오류 (UB) 컴파일 시 차단 (보장) 컴파일/런타임 차단 (보장) 수학적으로 부재 증명
데이터 경쟁 컴파일 시 차단 (보장) 런타임 차단 (보장) 수학적으로 부재 증명
정수 오버플로 panic (디버그) / 순환 (릴리즈) 런타임 예외 (회복 가능) 수학적으로 부재 증명
배열 범위 초과 panic (회복 불가능한 중단) 런타임 예외 (회복 가능) 수학적으로 부재 증명
논리적 오류 프로그래머 책임 계약 기반 설계로 일부 방지 계약에 따라 부재 증명 가능


결론: 안전성 스펙트럼에서의 위치


이 비교 분석은 러스트의 안전성 모델이 ‘안전성’ 스펙트럼의 특정 지점에 위치함을 보여줍니다. SPARK가 ‘수학적 증명’을 위해 개발자의 명시적인 증명 노력(주석, 계약 명시 등)과 전문 도구 활용을 요구하는 반면, 러스트는 일부 보증 범위(UB 방지)에 집중하고 개발자의 학습 곡선(빌림 검사기)을 비용으로 지불하는 방식으로 자동화된 안전성을 제공합니다.

두 기술은 각기 다른 공학적 문제에 대한 해법을 제시하며, 러스트의 안전성을 C/C++만을 비교 대상으로 평가하는 것은 시스템 프로그래밍의 전체 스펙트럼을 파악하는 데 한계를 가질 수 있습니다.



4.3 설계 철학 비교: 소유권 모델과 계약 기반 설계


프로그래밍 언어는 정확성(correctness)을 보장하기 위해 각기 다른 설계 철학을 채택합니다. 러스트가 사용하는 소유권(ownership) 및 빌림(borrowing) 모델은 컴파일 시점에 특정 유형의 오류를 자동으로 방지하는 데 중점을 둡니다. 반면, Ada/SPARK와 같은 언어에서 활용하는 계약 기반 설계(design by contract)는 개발자가 명시한 논리적 ‘계약’을 도구가 검증하는 방식을 사용합니다.

이 두 철학의 차이점과 각각의 공학적 상충 관계를 분석하기 위해, 컴퓨터 과학의 자료구조인 이중 연결 리스트(doubly-linked list) 구현을 사례 연구로 사용하고자 합니다.


1. 접근법 1: Rust의 소유권 모델


이중 연결 리스트는 각 노드(Node)가 이전 노드와 다음 노드를 상호 참조하는 구조를 가집니다. 다른 언어에서 포인터나 참조를 사용해 구현될 수 있는 이 구조는, 러스트의 기본 규칙과 직접적으로 충돌합니다. 러스트의 소유권 시스템은 기본적으로 순환 참조(reference cycle)나 단일 데이터에 대한 다중 가변 참조를 허용하지 않기 때문입니다.

따라서, 이 구조를 참조로 직접 표현하려는 노드 정의는 빌림 검사기(borrow checker)에 의해 컴파일 오류로 처리됩니다.

// 컴파일되지 않는 코드 struct Node<'a> { value: i32, prev: Option<&'a Node<'a>>, next: Option<&'a Node<'a>>, }

이러한 제약을 ‘안전한(safe)’ 러스트 코드 내에서 해결하기 위해서는, 언어가 제공하는 특정 기능들을 사용해야 합니다. 즉, 공유 소유권을 위한 Rc<T>, 내부 가변성(interior mutability)을 위한 RefCell<T>, 그리고 순환 참조를 끊기 위한 Weak<T>를 조합하여 사용합니다.

// Rc, RefCell, Weak를 사용한 구현 예시 use std::rc::{Rc, Weak}; use std::cell::RefCell; type Link<T> = Option<Rc<Node<T>>>; struct Node<T> { value: T, next: RefCell<Link<T>>, prev: RefCell<Option<Weak<Node<T>>>>, }
  • 분석: 이 접근법은 컴파일러가 데이터 경쟁(data race)과 같은 특정 유형의 동시성 문제를 자동으로 방지하는 이점을 제공합니다. 소유권 규칙은 특정 메모리 안전 규칙을 강제하며, 이중 연결 리스트와 같이 공유 상태가 필요한 경우는 개발자가 Rc, RefCell 등을 사용하여 해당 상태를 명시적으로 처리하도록 유도합니다. 이 과정에서 발생하는 인지적 비용(cognitive cost)과 코드의 장황함(verbosity)이 이 설계 철학의 비용입니다. 개발자의 초점은 문제의 논리적 구조보다, 컴파일러의 규칙을 만족시키는 방법에 더 집중될 수 있습니다.


2. 접근법 2: Ada/SPARK의 포인터 및 계약 기반 설계


Ada는 access 타입을 통해 C/C++과 유사한 포인터 사용을 지원하며, 이중 연결 리스트의 구조를 표현할 수 있습니다.

-- Ada를 사용한 표현 type Node; type Node_Access is access all Node; type Node is record value : Integer; prev : Node_Access; next : Node_Access; end record;

기본적으로 Ada는 널 포인터(null access) 역참조와 같은 오류를 런타임에 검사하여 Constraint_Error 예외를 발생시킴으로써 안전성을 확보합니다.

여기서 더 나아가, Ada의 부분집합인 SPARK는 계약 기반 설계를 통해 런타임 오류의 부재를 컴파일 시점에 수학적으로 증명하는 방법을 제공합니다. 개발자는 프로시저(procedure)나 함수에 사전 조건(precondition, Pre)과 사후 조건(postcondition, Post)을 명시하고, 정적 분석 도구는 이 계약을 코드가 항상 만족시키는지를 검증합니다.

-- SPARK 계약을 통한 안전성 증명 예시 procedure Process_Node (Item : in Node_Access) with Pre => Item /= null; -- 'Item은 null이 아니다'라는 계약을 명시
  • 분석: 이 접근법은 C/C++과 유사한 포인터 모델을 통해 개발자가 자료구조를 표현할 수 있게 합니다. 안전성은 런타임 검사 또는 개발자가 직접 작성하는 명시적 계약과 정적 분석 도구의 증명을 통해 확보됩니다. 이 설계 철학의 비용은 개발자가 모든 잠재적 오류 경로를 고려하고, 이를 형식화된 계약으로 작성해야 하는 책임과 노력입니다. 계약이 누락되거나 잘못 작성될 경우, 안전성 보증은 불완전해질 수 있으며, 이는 자동화된 규칙에 의존하는 방식과는 다른 종류의 위험을 내포합니다.


3. 설계 철학 비교 및 결론


두 접근법은 소프트웨어의 정확성을 확보하기 위한 책임과 비용을 각기 다른 주체와 시점에 배분합니다.


구분 러스트 (Rust) Ada/SPARK
안전성 확보 주체 컴파일러 (암묵적 규칙의 자동 강제) 개발자 + 도구 (명시적 계약 작성 및 정적 증명)
기본 패러다임 제한적(restrictive by default), 예외적 허용(opt-in complexity) 허용적(permissive by default), 계약을 통한 제약(opt-in safety proof)
주요 비용 특정 패턴 구현 시의 인지적 부하(cognitive overhead) 및 코드 복잡성 모든 상호작용에 대한 형식적 명세(formal specification) 작성 필요
주요 이점 데이터 경쟁과 같은 특정 오류 클래스의 자동 방지 개발자의 설계 의도 직접 표현 및 광범위한 논리적 속성 증명 가능


결론적으로, 러스트의 소유권 모델은 ‘혁신’ 또는 ‘결함’이라는 이분법적 시각으로 평가되기보다, 장점과 그에 상응하는 비용을 가진 하나의 설계 철학으로 분석됩니다. 이 철학은 특정 유형의 버그를 예방하는 기능을 가지며, 그 과정에서 개발자에게 학습 비용과 특정 문제에 대한 해결 방식을 요구하는 상충 관계를 내포하고 있습니다. 언어의 적합성은 해결하려는 문제의 종류, 팀의 역량, 그리고 프로젝트가 우선시하는 가치(예: 자동화된 안전성 보증 vs. 설계 유연성)에 따라 다르게 평가될 수 있습니다.