Hacker News 의견

• 소프트웨어의 형식적 검증은 소프트웨어 유형과 개발 프로세스에 크게 의존함. 대부분의 소프트웨어 프로젝트는 형식적 요구 사항과 호환되지 않음

  • 소프트웨어 개발과 설계가 종종 함께 진행되지만, 이는 형식적 방법에 적합하지 않음
  • 항공우주 소프트웨어와 같은 안전이 중요한 시스템은 형식적 검증의 이점을 크게 누릴 수 있음

• 형식적 방법이 소프트웨어의 복잡성을 해결할 수 있다는 주장은 자주 등장함

  • 학문적 접근 방식을 선호하는 사람들에게는 매력적일 수 있음
  • 그러나 형식적 방법이 실제로 문제를 해결하는 방법에 대한 설득력 있는 사례는 부족함
  • TLA와 같은 도구를 배우면 유용성을 이해할 수 있다는 암시가 있음

• 형식적 방법에는 두 가지 주요 유형이 있음: 코드와 분리된 외재적 기술과 코드와 함께하는 내재적 기술

  • 내재적 기술은 코드의 기능적 수준에서 작동하며, 외재적 기술은 코드 모델을 형식적으로 분석함
  • 현재 형식적 방법 연구의 황금기에 있으며, 내재적 기술이 더 주목받고 있음

• 경량 형식적 방법은 코드베이스와 함께 유지할 수 있으며, 단위 테스트보다 더 많은 통찰력을 제공함

  • 이 접근 방식은 일반적인 소프트웨어 개발 관행과 잘 맞음

• 형식적 소프트웨어 검증은 여전히 매우 어려운 작업이며, 극단적인 경우에만 가치가 있음

  • 전문가 수준의 지식이 필요하며, 대부분의 시스템에서는 매우 복잡함
  • Lean과 같은 도구를 배우는 것은 어렵지만, 문서화가 잘 되어 있음

• 형식적 방법에 대한 많은 기사는 컨설턴트를 위한 리드 생성처럼 느껴짐

  • 형식적 방법이 실제로 높은 품질의 코드를 생성할 때까지 기다려야 함

• 경량 형식적 방법 중 하나로 Linear Temporal Logic을 사용한 추적 검증이 있음

  • 이벤트를 기록하고 실행 추적에서 조건을 실행하는 간단하고 강력한 방법임

• 현대의 형식적 방법인 TLA+와 Alloy는 Python만큼 배우기 쉬움

  • 많은 클라우드 시스템이 이러한 도구로 검증되었음 (예: Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB)