AI·바이브코딩 기술 트렌드

테스트 말고 증명 — 버그가 없음을 수학으로 보장하는 언어 F* 이야기

'테스트는 버그가 있다는 것은 보여줄 수 있어도, 없다는 것은 증명할 수 없다.' 컴퓨터과학자 다익스트라의 유명한 말인데요. 테스트 케이스를 아무리 많이 짜도 결국 우리가 생각해낸 입력만 검사할 뿐, 생각하지 못한 입력에서 터지는 버그는 못 잡아요. 그런데 접근을 아예 뒤집어서, 코드가 명세대로 동작한다는 사실 자체를 수학적으로 증명해버리는 분야가 있어...