Hacker News 의견

해커뉴스 댓글 모음 요약

• 자동 번역 도구의 신뢰성

  • 자동 번역 도구가 신뢰를 얻음. coq-of-rust는 Rust로 작성되었고, Coq로 변환하여 올바름을 증명할 수 있음. 이는 Ken Thompson의 공격을 방지하는 방법과 유사함.

• 프로그램 크기와 검증

  • Coq 같은 반자동 증명 시스템으로 검증된 프로그램 크기는 작음. 100% 보증 비용이 99.9999% 보증 비용의 10배가 될 수 있음.

• 번역 과정의 오류 가능성

  • 코드의 Coq 번역 과정에서 오류가 발생할 가능성이 높음. 원본 코드에 대한 검증의 유효성을 의심함.

• 암호화폐 관련 게시물

  • 암호화폐 관련 내용이 적은 블로그 게시물을 제출함. Python에 대한 유사한 접근법을 다룬 게시물도 있음.

• 형식 검증의 한계

  • 형식 검증된 C 컴파일러에서 버그를 발견한 사례를 기억함. Coq 자체와 번역에 대한 신뢰성 문제를 제기함.

• Rust의 형식 검증

  • Rust의 기본 라이브러리가 형식 검증되면, 안전하지 않은 코드를 사용하지 않는 한 메모리 처리에 대한 형식 검증 품질을 얻을 수 있는지 궁금해함.

• 형식 검증 사양 작성

  • 형식 검증 사양 작성이 더 복잡한 속성 테스트 작성과 유사한지 궁금해함. 속성 테스트 작성이 어렵고 시간이 많이 걸림.

• 다른 접근법과의 비교

  • Aeneas나 RustHornBelt와의 접근법 차이를 비교해달라는 요청. 포인터와 가변 대여를 어떻게 처리하는지 궁금해함.

• Rust의 커널 채택

  • 이러한 노력이 Rust의 커널 채택을 가속화할 수 있을지 궁금해함.

• F*의 Rust 백엔드 추가

  • F*에 Rust 백엔드를 추가하는 데 얼마나 많은 작업이 필요한지 궁금해함.