이론적으로 프로그램의 올바름을 증명할 수 있는 여러 언어 중에서, 국제 표준을 보유한 언어는 Ada입니다. SPARK Ada는 Ada 언어의 서브셋(subset)으로, 안전-critical 시스템에서의 정형 검증을 위해 개발되었으며, Ada는 ISO/IEC 8652와 같이 국제 표준으로 채택되어 있습니다.

반면에 Coq, Agda, Idris, F\* 등은 매우 강력한 정형 검증 도구와 의존성 타입 기능을 제공하지만, 이들은 주로 연구 및 실험적인 용도로 사용되며 ISO와 같은 공식적인 국제 표준을 갖추지 않습니다.

따라서 국제 표준이라는 관점에서 본다면, SPARK Ada가 유일한 선택이며, 그 기반이 되는 Ada의 표준 덕분에 시스템 신뢰성과 안전성 측면에서 확실한 기반을 제공합니다.

구글 제미니

이론적으로 100% 버그 없음을 입증할 수 있는 언어로 어떤 것들이 있는가?

이론적으로 100% 버그 없음을 입증할 수 있는 언어들은 주로 정형 검증이라는 수학적 기법을 활용할 수 있도록 설계되었거나, 강력한 타입 시스템과 정적 분석 도구를 제공하는 언어들입니다. 이러한 언어들을 사용하면 프로그램이 명세된 요구사항을 정확히 만족하는지 수학적으로 증명할 수 있습니다.

주요한 언어들은 다음과 같습니다.

1. SPARK Ada: 이 책에서 다루고 있는 SPARK는 Ada 프로그래밍 언어의 하위 집합으로, 정형 검증을 위해 특별히 설계되었습니다. SPARK와 함께 제공되는 도구(예: GNATprove)를 사용하면 개발자는 작성한 코드의 특정 속성(예: 런타임 오류의 부재, 명세 준수 등)을 수학적으로 증명할 수 있습니다.

2. Coq: Coq는 정리 증명 보조 도구 (Proof Assistant) 이자 프로그래밍 언어입니다. 수학적 정의, 실행 가능한 알고리즘, 정리를 작성하고, 대화식으로 형식적인 증명을 개발하는 데 사용됩니다. Coq로 작성된 프로그램은 수학적으로 검증되었음을 보장할 수 있습니다.

3. Isabelle/HOL: Isabelle은 또 다른 정리 증명 보조 도구이며, HOL(Higher-Order Logic)은 그 안에서 주로 사용되는 논리 체계입니다. Isabelle/HOL을 사용하여 수학 이론을 형식화하고, 검증된 소프트웨어를 개발할 수 있습니다.

4. F:* F*은 프로그램 검증을 목표로 설계된 함수형 프로그래밍 언어입니다. 정련 타입(Refinement Types) 시스템을 지원하며, 프로그램의 속성을 증명하는 데 사용됩니다. Project Everest와 같은 프로젝트에서 검증된 HTTPS 스택을 구축하는 데 활용되었습니다.

5. Agda: Agda는 의존 타입 (Dependent Types) 을 지원하는 프로그래밍 언어이자 정리 증명 보조 도구입니다. 의존 타입은 값에 따라 타입이 달라질 수 있도록 하여 매우 정밀한 명세와 증명을 코드의 일부로 작성할 수 있게 합니다.

6. Haskell (특정 확장 사용 시): Haskell 자체는 100% 버그 없음을 보장하는 언어는 아니지만, Liquid Haskell과 같은 도구를 사용하면 정련 타입 검사를 통해 코드의 안전성을 높이고 특정 속성을 증명할 수 있습니다.

7. Why3: Why3는 연역적 프로그램 검증을 위한 플랫폼입니다. 프로그램을 명세하고 구현하기 위한 언어와 다양한 자동 증명기와 정리 증명 보조 도구를 사용하여 프로그램의 정확성을 증명하는 시스템을 제공합니다.

주의할 점:

• 이론적으로는 가능하지만, 실제 복잡한 소프트웨어에서 100% 버그 없음을 완전히 증명하는 것은 매우 어렵고 많은 노력이 필요합니다.
• 정형 검증은 일반적으로 특정 명세에 대해 코드가 정확히 작동하는지를 증명하는 것이며, 명세 자체의 오류나 누락은 발견하지 못할 수 있습니다.
• 이러한 언어들은 일반적인 프로그래밍 언어에 비해 학습 곡선이 높고, 개발 과정이 더 엄격할 수 있습니다.

이러한 언어들은 높은 수준의 안전성과 신뢰성이 요구되는 분야(예: 항공 우주, 국방, 의료 시스템 등)에서 주로 사용됩니다.

그 중 국제표준이 있는 언어는?

제시해주신 언어 중에서 국제 표준이 있는 언어는 다음과 같습니다.

• Ada (및 SPARK Ada): Ada 프로그래밍 언어는 ISO/IEC 8652라는 국제 표준을 가지고 있습니다. SPARK Ada는 Ada의 하위 집합이기 때문에, Ada 표준의 적용을 받습니다. 특히 안전성과 신뢰성이 중요한 분야에서 Ada의 국제 표준은 중요한 의미를 가집니다.

• Haskell: Haskell은 엄밀히 말하면 ISO 표준은 아니지만, Haskell Report라는 공식적인 명세가 존재하며, 이는 사실상의 표준으로 간주됩니다. 예를 들어, Haskell 98 Report, Haskell 2010 Report 등이 있습니다.

다른 언어들(Coq, Isabelle/HOL, F*, Agda, Why3)은 주로 연구 목적으로 개발되었거나 특정 커뮤니티에서 주로 사용되며, 공식적인 국제 표준은 없습니다. 이들의 명세는 주로 해당 언어의 개발 팀이나 커뮤니티에서 관리합니다.

따라서 국제 표준을 기준으로 선택하신다면 **Ada (및 SPARK Ada)**를 고려해볼 수 있습니다.