Hacker News 의견

• Verus를 사용하여 공식적으로 검증된 Kubernetes 컨트롤러를 작성함
  • 컨트롤러가 결국 요청된 desired state로 클러스터를 조정할 것이라는 liveness 속성을 증명할 수 있음
  • 정확성을 명시하는 데에는 미묘한 점과 뉘앙스가 많이 있음 (desired state 요구사항의 빠른 변화, 비동기성, 장애 등)
  • 코드는 GitHub 링크에 있으며, OSDI 2024에 게재 예정인 논문과 연결됨
• Verus를 향한 작은 디딤돌로, Rust의 debug_assert를 사용하여 사전조건과 사후조건을 추가할 수 있음
  • Rust 컴파일러는 기본적으로 프로덕션 빌드에서 이를 제거함
  • Verus 튜토리얼의 예제와 debug_assert를 사용한 런타임 체크 예제 제공
• "코드의 정확성 검증"과 "코드의 정확성 증명"의 차이점에 대한 초보자 질문
  • CS/수학 배경이 약한 실무 프로그래머를 위한 코드 "증명"에 대한 좋은 학습 자료가 있는지 궁금함
  • "제로 지식" 증명이 왜 중요한지, 왜 이것이 그렇게 관련이 있는지 매우 궁금함
• Rust 표준은 C/C++, Common Lisp, Ada/SPARK2014와 같이 아직 없음
  • 이는 Ada/SPARK2014 등을 위해 개발된 검증 도구와 비교할 때 움직이는 목표임
• Dafny는 Rust로 컴파일할 수 있는 "검증 인식 프로그래밍 언어"임 (GitHub 링크)
• 주요 기여자 중 한 명이 취리히 Rust 밋업에서 Verus에 대한 훌륭한 발표를 함 (YouTube 링크)
  • "ghost" 코드가 프로그램에 깔끔하게 맞는 것이 인상적이었음 (Ada를 약간 연상시킴)
• Verus와 SPARK의 비교
  • 동일한 일반 클래스의 검증기인가? Verus가 Ada용 검증기가 아닌 Rust용 검증기라는 점 외에 어떤 차이가 있는가?
• Verus에 정통한 사람이 Verus와 Lean4의 성능과 표현력을 비교해 줄 수 있는지?
  • Verus는 SMT 기반 검증 도구이고, Lean은 대화형 증명기이자 SMT 기반 도구라고 이해함
  • 그러나 형식 검증 분야에 대한 이해도는 제한적이므로, 소프트웨어 형식 기법에 정통한 사람의 의견을 듣는 것이 좋겠음
• Verus와 Kani의 관계가 있는지? 다르게 작동하는지? (Kani GitHub 링크)
• 결과 코드가 여전히 바닐라 Rust 도구를 사용하여 컴파일할 수 있는 유효한 Rust 코드가 되도록 구현하는 방법이 있는지?