형식적 기법: 단지 좋은 공학 실천인가? (2024)

 (brooker.co.za)
1P by GN⁺ | ★ favorite | 댓글 1개
  • 대규모·분산·중요 저수준 시스템에서 형식적 기법은 정확성만을 위한 추가 절차가 아니라 시간과 비용을 줄이는 공학 실천으로 봐야 함
  • 소프트웨어는 설계와 구현이 쉽게 뒤섞여, 늦은 설계 수정이 곧 구현 재작업과 API 변경 비용으로 이어짐
  • 구현 전에 동작과 인터페이스를 구체적으로 검토하면 버그 밀도와 프로덕션 이후 문제를 줄이고, 더 빠르게 올바른 설계에 도달할 수 있음
  • 빠르게 변하는 사용자 요구나 UI·문서·가격 로직처럼 형식화하기 어려운 영역에서는 전면적인 사전 형식 설계의 효용이 낮아질 수 있음
  • TLA+, P 같은 도구는 설계 단계에서 최적화와 제약을 검토해 정확성과 성능의 트레이드오프를 줄이는 데도 쓰일 수 있음

좋은 공학 실천으로서의 형식적 기법

  • 형식적 기법은 좋은 소프트웨어 엔지니어링 실천의 중요한 일부임
  • 특히 대규모 시스템, 분산 시스템, 중요한 저수준 시스템을 다루는 엔지니어에게 적용 가치가 큼
  • 공학은 궁극적으로 시간과 비용을 최적화하는 활동이라는 전제에서 출발함
    • 성능, 확장성, 지속가능성, 효율성도 함께 고려됨
  • 형식적 기법은 싸거나 쉽지 않고 모든 개발 방식에 잘 맞지도 않지만, 비용만 늘린다는 직관은 항상 맞지 않음

비용을 줄이는 두 가지 경로

  • 첫 번째는 재작업 감소임
    • 소프트웨어는 다른 공학 분야와 달리 설계와 구축이 동시에 일어나기 쉬움
    • 설계가 충분히 진행되지 않아도 구현을 시작할 수 있음
    • 이런 가변성은 소프트웨어의 강점이지만, 설계 반복을 구현 반복으로 바꿔 비용을 키울 수 있음
  • 두 번째는 변경 비용 관리임
    • API나 시스템에 고객이 생기면 변경은 훨씬 더 비싸고 어려워짐
    • Hyrum’s Law에 따르면 충분한 수의 API 사용자가 있을 때 계약 내용과 관계없이 관찰 가능한 모든 동작에 누군가 의존하게 됨
  • API로 시스템 동작을 격리하는 것은 소프트웨어 엔지니어링의 중요한 아이디어지만, 사용자가 구현 세부사항까지 의존할 수 있다는 한계가 남아 있음
  • API 뒤의 시스템을 완전히 재구현할 수는 있어도, 추상화가 변경 비용 자체를 없애지는 못함
  • 형식적 설계 작업은 재작업 비용을 줄이고 인터페이스 변경을 더 이른 시점에 처리하게 해 소프트웨어 구축 속도와 효율을 높일 수 있음

형식 설계가 잘 맞는 시스템

  • 모든 소프트웨어에 같은 방식으로 적용되지는 않음
  • 빠르게 진화하거나 형식화하기 어려운 사용자 요구가 많은 소프트웨어에서는 사전 설계의 가치가 약해질 수 있음
    • UI, 웹사이트, 가격 로직 구현 등이 여기에 해당함
    • 이런 영역에서는 지속적인 재작업이 많아 사전 설계 비용이 커질 수 있음
  • 애자일의 기반 아이디어는 구현과 요구 수집을 병렬로 진행해 출시까지의 시간을 줄이는 것임
    • 요구 수집이 계속되는 경우에도 구현을 완료할 수 있게 함
    • 많은 경우 이런 병렬 개발 방식은 최적이거나 진행을 가능하게 하는 필수 조건임
  • 반대로 대규모, 분산, 저수준 시스템의 많은 부분은 요구사항이 잘 이해되어 있음
    • 최소한 충분히 큰 정적 요구사항 부분이 존재함
    • 이 경우 사전 형식 설계가 구현 단계와 프로덕션 이후의 재작업 및 버그 밀도를 상당히 줄일 수 있음
  • 요구사항이 물리 법칙에 가까울수록 설계와 형식 설계의 가치가 커지고, 사용자 의견에 가까울수록 그 가치는 작아짐

요구사항 문서화와 형식화의 한계

  • 사용자 요구사항을 명확히 적는 일은 형식적이든 비형식적이든 매우 가치가 큼
  • 요구사항을 적지 않으면 시간이 낭비되고, 사람들이 서로 다른 방향으로 움직이면서 마찰이 생길 수 있음
  • 모든 인간 요구사항을 형식적으로 명세하기는 어렵거나 경제적이지 않을 수 있음
    • UI 미적 요구사항
    • 문서 가독성
    • API 이름 일관성
  • 형식적 접근에 대한 의견 차이는 형식적 접근이 무엇이며 어떤 방식으로 가치가 있는지에 대한 서로 다른 생각에서도 나옴
  • UML처럼 코드를 방대한 도식으로 옮기는 방식은 어려운 질문을 직접 다루지 못하면 가치가 낮아질 수 있음
    • 나쁜 방식이나 나쁜 도구로 수행하면 가치 있는 작업도 쓸모없어질 수 있음

현장에서 유용한 형식적 기법과 도구

  • 형식적 기법과 자동 추론은 넓은 분야이며 다양한 도구가 있음
  • 대형 클라우드 시스템 영역에서 유용했던 도구 묶음은 다음과 같음
    • P, TLA+, Alloy 같은 명세 언어와 관련 모델 체커
    • turmoil 같은 결정적 시뮬레이션 도구
      • 퍼징과 함께 테스트를 통해 상태 공간을 체계적으로 탐색하는 데 사용됨
    • Dafny 같은 검증 친화적 프로그래밍 언어와 Kani 같은 코드 검증기
    • 수치 시뮬레이션 기법
    • 화이트보드나 설계 문서에서 결정표, 진리표, 명시적 상태 머신을 그리는 형식에 가까운 방법
  • Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3는 경량 형식 기법을 살펴보는 출발점임
  • 구현 검증만이 유일한 목표는 아님
    • TLA+와 P 같은 도구는 구현 전에 설계를 더 빠르고 구체적으로 검토하는 데 큰 가치가 있음

더 빠른 소프트웨어를 더 빠르게 만들기

  • 2015년 How Amazon Web Services Uses Formal Methods 작성 당시 초점은 주로 정확성이었음
    • 설계의 안전성 및 활성 속성을 검증하는 것
    • 올바른 설계에 더 빨리 도달하는 것
  • 내부 락 관리 시스템에 TLA+를 사용하던 팀의 사례에서는 “공격적인 최적화를 검증”했다는 점이 중요했음
  • TLA+ 같은 도구는 시스템을 더 빨리 만들게 할 뿐 아니라, 더 빠른 시스템을 만들게 할 수 있음
    • 가능한 최적화를 빠르게 탐색함
    • 정말 중요한 제약을 찾음
    • 제안한 최적화가 올바른지 확인함
  • 많은 경우 형식적 기법은 시스템이 빠지기 쉬운 정확성과 성능의 어려운 트레이드오프를 줄여줌

설계 단계에서 쓰는 도구의 가치

  • 시스템 설계를 생각하는 데 도움이 되는 도구를 설계 단계에 사용하면 소프트웨어 개발 속도를 크게 높일 수 있음
  • 위험을 줄이고, 처음부터 더 최적화된 시스템을 만들 수 있게 함
  • 대규모·복잡한 시스템을 만드는 엔지니어에게 형식적 기법은 좋은 공학 실천의 일부임

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • 소프트웨어 정형 검증은 글에서도 인정하듯 소프트웨어의 종류와 개발 프로세스에 크게 좌우됨
    정형 검증을 쓰려면 소프트웨어 동작에 대한 정형 요구사항이 있어야 하는데, 대부분의 프로젝트와 설계 철학은 여기에 맞지 않음. 무엇을 원하는지도 확실하지 않은 상태에서 개발과 설계가 함께 진행된다면 정형 기법은 적용하기 어렵다. 다만 작고 안전이 중요한 시스템처럼 사전 명세에 의존하는 영역은 큰 이득을 볼 수 있고, 항공우주 소프트웨어가 대표적임

    • 그렇게까지 틈새라고 느끼진 않았음. 사람들이 말하는 비용은 지난 수십 년 동안 많이 내려갔고, TLA+나 Alloy 같은 도구는 개발자에게 일주일 안에도 가르쳐 봤음
      요즘은 박사 학위나 수년의 연구가 있어야 익히는 기술이 아니고, 기본적인 고수준 명세를 쓰는 것도 마찬가지임. 모델 검사기를 쓰면 모델링하는 시스템에 대해 무언가를 배우게 되고, 문서화나 교육 용도로만 써도 유용함. 정형 기법의 근본적인 힘은 끝까지 생각하게 만든다는 데 있음. 많은 개발자가 자기 머리, 타입 검사기, 약간의 단위 테스트만으로 동시성 알고리즘을 구현할 수 있다고 믿지만, 모델 검사기를 돌린 뒤 설계와 가정에서 오류를 발견하면 겸손해질 수밖에 없음. 생각보다 작은 분산 시스템은 많고, 상태 공간은 정형화해 보기 전 예상보다 훨씬 큰 경우가 많음
    • 전부 아니면 전무가 아님. 완전히 명세화되지 않은 매우 제품 지향 백엔드를 다루지만, 그중 일부는 정형적으로 명세했음
      예를 들어 아주 까다로운 상태 기계에 속성 기반 테스트를 붙여서, 어떤 이상한 입력으로 엔드포인트를 호출하더라도 내부 상태 기계가 유효하지 않은 전이를 하지 않도록 확인했음. 주변 코드는 정형 명세가 없지만 상태 기계에는 있었기 때문에 가능했고, 전통적인 단위 테스트로는 절대 못 잡았을 미묘한 버그도 찾았음
    • “정형”은 “컴퓨터가 해석할 수 있는 언어로 쓰였다”는 뜻이고, 프로그래머가 하는 일이 바로 그것임. 코드를 쓰는 것은 프로그램 동작의 정형 명세를 쓰는 것이며, 정의상 모든 소프트웨어는 그렇게 해야 함
      다만 정형 기법의 이득을 보려면 프로그램 동작을 프로그램 자체가 아닌 다른 것과 비교해야 하고, 그 다른 것도 정형 언어로 쓰여야 함. 원하는 동작을 정확히 이해해야 하지만, 소프트웨어 전체 동작을 모두 덮을 필요는 없음. 자동화된 단위 테스트도 정형 명세이고, 이를 실행하는 것은 정형 검증 방법임. 일반적으로 말하는 정형 기법보다 약한 명세와 약한 검증일 뿐, 개념적으로나 실무적으로 명확한 질적 차이가 있는 것은 아님. 테스트가 적용 가능한 소프트웨어라면 더 풍부한 정형 명세 방법도 적용 가능할 가능성이 크고, 비용 대비 효과는 테스트를 배우듯 시행착오로 익히게 됨
    • 원하든 원하지 않든 요구사항은 생기게 되어 있음. 요구사항 공학 단계에서 발견해 간단한 텍스트 문서로 검증하고 충돌을 정리하든, 코딩하면서 잘못 만든 뒤 알게 되든, “스프린트 리뷰”에서 고객이 발견하든 차이일 뿐임
      결국 “애자일”이라고 불리기 위해 돈과 시간을 얼마나 더 쓸 것인가의 문제임. 역설적으로 전통적인 요구사항 단계가 세 방식 중 가장 저렴하고, 변경 비용이 가장 싼 시점인 텍스트 한 줄을 바꾸는 단계에서 고객과 빠르게 수렴하므로 원래의 애자일 정신에도 가장 잘 맞음
    • 핵심은 사전 설계라기보다 정형화 가능성에 가까워 보임. 예를 들어 보험 청구 자동화 시스템은 보험사들의 동작이 명시되지 않은 경우가 많아 처음부터 설계할 수 없지만, 상호작용으로 정보를 얻으면서 자동화 시스템을 다듬을 수 있음
      그래도 모든 경우를 빠뜨리지 않았는지, 시스템 안에 모순이 없는지 확인하는 이득은 얻을 수 있음

  • 정형 기법에 대해 “소프트웨어는 크고 복잡하며 맞히기 어렵다, 그러므로 정형 기법”이라는 논리를 자주 봄
    한편으로는 이게 사실이었으면 좋겠음. 학문적으로 배우는 방식에 강해서 개인적으로도 이득이고, 실무적으로도 소프트웨어가 실제로 복잡해 실패했을 때 원인을 찾아 헤매는 것이 답답하기 때문임. 하지만 정형 기법이 그 문제를 어떻게 해결하는지 설득력 있게 보여주는 경우는 거의 없음. 이 글은 현대의 “설계” 대부분이 시간 낭비라고 짚는 점에서는 낫지만, TLA가 UML보다 왜 나은지는 충분히 설명하지 않음. 마치 몇 달 혹은 몇 년을 TLA에 투자하면 깨달음을 얻고, 깨닫지 못한 사람에게는 설명할 수 없는 방식으로 유용함을 알게 된다는 암시처럼 들림. 미적분이나 베이즈 통계도 그런 면이 있어 불가능한 얘기는 아니지만, 결국 “정말 그렇게 유용하다면 더 많은 사람이 썼고 이점이 저절로 드러났을 것”이라는 프로젝트 관리자식 판단으로 돌아가게 됨. 오래전부터 있었지만 널리 자리 잡지 못했다면 이유가 있을 가능성이 큼

    • UML이 쓸모없는 이유는 같은 다이어그램도 사람마다 다르게 이해하고, 매우 복잡한데도 검사 가능하지 않아서 자기모순이 있거나 말이 안 되는 UML 다이어그램을 만들 수 있기 때문이라고 봄
      생각하기 어려운 문제를 만나면 어떤 “방법”을 쓰게 됨. 통신 프로토콜이라면 상태 기계로 설명하는 것이 좋고, TLA는 그 틈새에 더 잘 맞음. 최근에는 그 정도 노력을 정당화할 문제가 많지 않았지만, 그런 문제가 생기면 엄청난 가치가 있음. 도메인 특화 언어도 마찬가지로, 여러 문제를 피하려면 직접 파서를 짜기보다 파서 프레임워크를 쓰는 편이 훨씬 낫다. 지금 재작업의 대부분은 요구사항 변경과 고객이 실제로 원하는 것을 모른 채 “그건 아니야”라고 말하는 데서 옴. 요청하는 사람들이 자기 요구의 함의를 충분히 생각하지 않는 것도 있지만, 좋은 결정을 내릴 지식이 한곳에 충분히 모이지 않는 것이 더 큼
    • 정형 기법이 널리 쓰이지 않는 이유는, 도메인 로직의 정확도를 98%에서 99.99% 로 올리기 위해 큰 시간과 비용을 들여야 하는 사업 영역이 실제로 많지 않기 때문이라고 봄
      정형 기법은 분명 큰 투자임. 다만 일반적으로는 자리 잡지 못했어도, 그 아이디어 일부는 현대 타입 시스템으로 들어왔음
    • 하드웨어 수업 맥락에서만 정형 검증을 접해 봤는데, 프로그래밍과 비슷하지만 비용 대비 효과가 완전히 다름. 물리 칩은 제작 후 쉽게 고칠 수 없고 설계 유형도 매우 다름
      받은 인상은 정형 검증기의 엄격함이 합리적인 시간과 메모리 안에 끝나야 한다는 이유만으로도 설계 복잡도에 한계를 부과한다는 것임. 어쩌면 정형 검증을 요구하는 진짜 승리는 “소프트웨어가 크고 복잡하고 맞히기 어렵다”는 문제를, 큰 복잡한 프로그램을 다루기 귀찮게 만들어 고치는 데 있을지도 모름
    • 이 개구리를 천천히 삶으려면 TLA를 가르치기보다 거기서 지혜를 훔쳐와야 함. 타입 시스템은 Hindley-Milner에서 많은 것을 빌려왔고, 그 자체가 정형적인 부분 증명임
      SAT나 TLA 기법을 이용해 입력 공간을 반복 가능하게 빠르게 줄이는 속성 기반 테스트의 후손을 보고 싶음. 파싱과 코드 커버리지를 통해 함수에 12를 넘기는 것이 11과 다른 분기를 탈 수 없지만, -1이나 2^17 < n < 2^32 같은 값은 다를 수 있음을 추론할 수 있어야 함
    • “정말 유용하다면 더 많은 사람이 썼을 것”이라는 논리는 어떤 분야에서도 좋지 않고, 소프트웨어 개발에서는 두 배로 나쁨
      아직도 대부분의 소프트웨어 프로젝트는 실패함. 이건 “시장 실패”가 아니라 그냥 “만드는 데 실패함”에 가까움

  • 정형 기법에는 크게 두 갈래가 있음. 코드 자체와 분리되어 보통 코드의 명세를 추론하는 외재적 기법과, 코드 안에 들어가 코드를 더 직접적으로 추론하는 내재적 기법임
    역사적으로 타입 시스템 같은 내재적 기법은 함수 수준에서 코드를 추론했고, Spin/P 같은 판정 가능한 모델 검사기 같은 외재적 기법은 오토마타 같은 형식주의로 기술된 코드 모델을 다뤘음. 지금은 정형 기법 연구의 황금기라고 보며, 타입 시스템 발전과 Verus 같은 프로젝트가 밀어붙이는 내재적 방법에 비해 외재적 기법은 점점 덜 선호되는 흐름으로 보임. https://github.com/verus-lang/verus

    • TLA+ 같은 도구는 아주 작은 명세 언어를 대상으로 하기 때문에 잘 동작함
      Rust처럼 발자국이 큰 언어에서 이게 어떻게 작동할지에 대한 질문은 봤지만 좋은 답은 아직 못 봤음. 더 읽어보고 싶음
    • 링크된 Verus 프로젝트도 정확성 명세를 직접 쓰게 한다면 그 구분이 왜 의미 있는지 잘 모르겠음
      내재적 기법이 별도의 명세를 작성하고 유지하지 않아도 되기 때문에 선호된다는 말처럼 들렸지만, 실제로는 그렇지 않음

  • 경량 정형 기법을 짚은 부분은 좋음. 코드베이스 옆에 proptest 전략 모음을 유지하는 것은 수작업 단위 테스트를 쓰는 것보다 훨씬 큰 투자가 아니지만, 넓은 커버리지와 작고 이해 가능한 실패 사례 덕분에 훨씬 나은 통찰을 줌
    무엇보다 이 접근은 일반적인 소프트웨어 개발 관행과도 잘 맞음. https://crates.io/crates/proptest

    • 요즘은 LLM으로 단위 테스트를 많이 생성함. 꽤 괜찮게 만들고, 조금 더 철저하게 하라거나 생각나는 경계 조건을 테스트하라거나 특정 조건을 처리하라고 지시할 수 있음
      좋은 테스트를 쓰는 방법과 거기에 들어가는 노력을 어느 정도 알지만, LLM은 나보다 훨씬 빠르게 더 나은 테스트를 만들 수 있음. 반복적이고 지루한 일을 하다 보면 인내심이 떨어지는 나보다 오히려 덜 대충 할 가능성이 큼. 소프트웨어 엔지니어라면 반복적으로 느껴지는 일은 자동화하려는 반사작용이 있어야 하고, 문서화도 요즘은 생성해서 더 자주 더 일찍 하게 됨. LLM은 정형 검증 채택에 작은 혁명을 일으킬 수도 있음. 올바른 명세 생성은 지루하면서도, 동작하는 코드·문서·힌트 같은 충분한 맥락이 있다면 LLM에게 비교적 쉬운 작업일 수 있음. 명세를 직접 전부 쓰기보다 생성하게 한 뒤 훑어볼 수 있다면 훨씬 더 할 마음이 생김. Rust를 쓴다는 것은 정확성을 중요하게 여긴다는 신호이기도 하고, 그 컴파일러는 정형 기법 없이 시스템이 아마 맞다는 것을 증명하는 데 가장 가까운 도구에 가까움. 컴파일러나 명시 타입도 없는 언어에 정형 기법을 덧붙이는 것보다 훨씬 쉬울 가능성이 큼
    • proptest나 qcheck는 정형 기법이 아니라 무작위 테스트임

  • 소프트웨어 정형 검증은 아직도 극단적인 경우가 아니면 가치가 있을 만큼 쓰기엔 너무 어려움. 반대로 하드웨어 정형 검증은 안 쓸 이유가 없는 수준임
    계속 배우려 하지만 대부분의 시스템에서는 “컴파일러를 직접 쓴 사람” 수준의 전문가여야 함. 예를 들어 varint 인코더/디코더를 증명하려 했는데 1~2바이트는 됐지만 그 이상은 안 됐음. 도움을 청하니 컴파일러 내부에서 루프를 5번만 펼친다는 식의, 도저히 알 수 없는 내부 세부사항 때문이었음. 최근 Lean을 배우고 있는데 마음에 들긴 하지만 이런 문서를 만나게 됨: “Definitional equality includes η-equivalence…” 같은 식임. Lean을 깎아내리려는 건 아니고, 오히려 대안들 중 문서가 나은 편으로 보임

    • FizzBee.io를 써봤는지 궁금함. Python 비슷한 문법을 쓰고 예제도 볼 만함: https://fizzbee.io/examples/two_phase_commit_actors/#complet...
      정형 기법이 꼭 복잡할 필요는 없음. 문제는 대부분의 정형 기법이 교수가 관심 있던 특정 주제를 보여주기 위한 학문적 연습처럼 설계됐다는 데 있음. TLA+도 논문 작성을 위해 설계된 쪽에 가깝고
    • 무서워 보이지만 그 개념들은 실제로는 전부 아주 단순하고, 이미 익숙한 것들일 가능성이 큼

  • 경량 정형 기법 중 널리 알려지진 않았지만 좋아하는 것은 선형 시간 논리를 이용한 추적 검증임: https://en.m.wikipedia.org/wiki/Linear_temporal_logic
    기본적으로 이벤트만 로깅하면 되고, 이벤트 기반 아키텍처에서는 사실상 공짜로 얻을 수도 있음. 그런 다음 실행 추적 위에 Always(Locked, Implies(Eventually(Unlocked))) 같은 술어를 돌리면 됨. 과거 추적에도 적용할 수 있고, 스트레스 테스트나 퍼징과 결합해 상태 공간을 탐색할 수도 있음. 단순하고 강력하며 널리 적용 가능하고, 모델 없이 술어만 있으면 됨

    • 사소한 구분이지만, 이건 시스템 추적의 일부 집합에 대해서만 공식을 확인하므로 테스트에 더 가까움
      정형 기법은 시스템 동작에 대한 포괄적인 근거를 함축함. TLA나 비슷한 시스템에서는 실제 시스템이 아니라 상태 기계이긴 해도, 그 출력은 LTL/CTL/TLA 속성이 시스템의 모든 동작, 즉 추적이나 추적 트리에 대해 성립한다는 증명임

  • 이전 논의는 2024년 6월에 있었음: https://news.ycombinator.com/item?id=40753989

  • 너무 느림. 계획은 곧 화석화이고, 어떤 문서든 애자일 법정에서 불리한 증거로 쓰일 수 있음

    • 논쟁적으로 말하면 “진짜 애자일”이 발견된다면 정형 기법은 그 정반대일 것임. 증명 가능하고 재현 가능한 것은 참된 신자들에게 신성모독이기 때문임

  • 정형 기법에 대해 읽은 글 대부분은 컨설턴트의 잠재 고객 확보처럼 느껴짐
    그 자체는 괜찮지만, 직원이나 동료에게 교육 패키지를 사거나 나를 고용하면 나쁜, 심지어 무책임하게 위험한 프로그래밍 습관을 고쳐주겠다는 식으로 정형 기법을 통한 깨달음에 도달한 듯 행동하면 불쾌함. 정형 기법이 명세에서 벗어날 수 없는 고품질 코드를 실제로 생성하게 되면 다시 이야기해 달라

    • https://en.wikipedia.org/wiki/SPARK_(programming_language)는 어떨까
    • “명세에서 벗어날 수 없는 고품질 코드를 생성”하면 유용하겠지만 근본 문제가 있음. 코드는 너무 구체적임
      정형 명세에서는 보통 그 정도 세부까지 지정하지 않고 시스템의 일반적인 동작을 지정함. 그래서 명세 하나가 미묘하게 다른 많은 프로그램에 대응하는 경우가 많음. 코드가 문서로 부족한 이유도 여기에 있음. 무엇이 의도된 선택이고 무엇이 우연한 선택인지 알 수 없기 때문임. 코드는 고수준 요구사항을 설명하기엔 너무 구체적임. 반대로 명세에 대해 프로그램을 검증하는 쪽은 구현 가능성이 더 큼

  • 현재 정형 기법 옹호자 중 일부는 정형 기법을 쓰지 않는 사람을 “게으르다”거나 “멍청하다”고 보고, 자신들은 “옳은 일을 한다”거나 “복잡한 언어를 숙달했다”는 이유로 우월함을 주장하려 함
    물론 전부는 아니고 좋은 사람들도 알지만, 일부는 사실 한 가지 재주만 있는 사람에 가깝다. 최근 몇 년간 배웠거나 시도한 다른 정형 기법 시스템을 물으면 “너무 바빠서” 새것을 배울 수 없다고 함. 최근 더 쓰기 쉬운 정형 기법으로는 Python 방언을 써서 의사코드처럼 읽히는 FizzBee, 더 쉬운 문법을 가진 Quint, C# 사용자에게 익숙한 문법의 P가 있음. 이 글의 저자도 정형 기법이 자기 문제의 절반만 해결한다고 쓴 적이 있음: https://brooker.co.za/blog/2022/06/02/formal.html
    하지만 거기서 말한 문제는 새롭지도 않은 PRISM이 이미 해결함. Brooker가 주변을 찾아보거나 배우려 하지 않을 뿐임

답변달기
GeekNews BeeBS 게시판 오픈! 자유로운 이야기와 소소한 일상을 함께 나눠보세요.