옛날 보안이 만들고 -> 버그 찾고 (pentest) -> 패치 하고 이 순서대로 진행했다면
만들 때부터 철저하게 설계해서 버그가 없도록 하는게 요새 추세임


이러한 설계를 위해 쓰는 것 중 하나가
프로그램에 여러 제약 조건을 걸어두고 코드가 만족하는지 보는거임


예를 들어서 min(a, b) 함수를 작성한다고 생각하자
그러면 x = min(a, b) 라고 했을 때 ((x == a) or (x == b)) and (x <= a) and (x <= b) 를 만족해야함
주어진 코드를 검사기가 분석해서 저 조건이 빠짐없이 맞는지 확인해줌


문제는 코드를 검사기에 직접적으로 넣을 수가 없고 검사기에 쓸 수 있는 적절한 형태(모델)로 변환시켜야 하는데
이 작업이 그냥 프로그래머가 하기는 힘들어서 전문가가 해야함
그런데 보통 그런분들은 코딩을 못함


결국 할 수 있는게 2가지인데
(1) 코드를 작성해서 툴을 이용해 모델로 변환, 검사기 돌림
이 때 검사기에서 해당 모델을 못 검사하는 경우가 있음. 그러면 모델을 바꿔서 하는 일은 같지만 검사가 가능하게 바꿔야하는데
프로그래머는 어떻게 고쳐야 할지 모르고, 전문가는 어디를 고쳐야 할지 모름;;


(2) 모델을 만들고 툴을 이용해 코드로 변경
이러면 코드가 비효율적이라서 느림


결국 마지막으로 선택한게 하스켈 같은 언어를 이용하는거임
하스켈은 프로그래머가 그나마 배울만하고
전문가도 알아먹을 수 있기 때문에 모델 만들기도 좋음


그래서 많이 이용된다