다익스트라가 초기에 인식한 문제는 프로그래밍은 어렵고, 프로그래머는 프로그래밍을 잘하지 못한다는 사실이었다.
모든 프로그램은 설령 단순할지라도 인간의 두뇌로 감당하기에는 너무 많은 세부사항을 담고 있었다. 아주 작은 세부사항이라도 간과하면 프로그램이 동작하는 것처럼 보이더라도 결국엔 예상 외의 방식으로 실패하곤 했다.
다익스트라는 증명이라는 수학적인 원리를 적용하여 이 문제를 해결하고자 했다. 그의 비전은 공리,정리, 따름정리, 보조정리로 구성되는 유클리드 계층구조를 만드는 것이었다. 다익스트라는 수학자가 유클리드 계층구조를 사용하는 방식을 프로그래머도 사용할 수 있다고 믿었다. 다시 말애 프로그래머는 입증된 구조를 이용하고, 이들 구조를 코드와 결합시키며, 그래서 코드가 올바르다는 사실을 스스로 증명하게 되는 방식이었다.
당연하게도 다익스트라는 이렇게 하려면 단순한 알고리즘에 대해 기본적인 증명을 작성할 수 잇는 기법을 보여줘야 한다는 사실을 깨달았다.
이 연구는 goto 문장이 모듈을 더 작은 단위에 대해 재귀적으로 분해한다고 가정했을 때, 이 과정에 방해가 되는 경우가 있다는 사실을 발견했다. 만약 모듈을 분해할 수 없다면, 합리적으로 증명할 때 필수적인 기법인 분할 정복 접근법을 사용할 수 없게 된다.
반면, goto 문장을 사용하더라도 모듈을 분해할 때 문제가 되지 않는 경우도 있다. 다익스트라는 이런 goto문의 좋은 사용 방식은 if/then/else, do/while과 같은 분기와 반복이라는 단순한 제어 구조에 해당한다는 사실을 발견했다. 모듈이 이러한 종류의 제어 구조만을 사용한다면 증명 가능한 단위로까지 모듈을 재귀적으로 세분화하는 것이 가능해 보였다.
이 세 가지로 구조적 프로그래밍을 증명할 수 있게 되었다.
단순한 열거법을 이용해 순차 구문(Sequential statement)이 올바름을 입증할 수 있다. 이 기법은 각 순차 구문의 입력을 순차 구문의 출력까지 수학적으로 추적한다.
이 접근법은 수학적 증명 방식과 다를 바 없다.
분기 의 경우 열거법을 재적용하는 방식이다. 먼저 분기를 통한 각 경로를 열거했다. 결과적으로 두 경로가 수학적으로 적적한 결과를 만들어낸다면, 증명은 신뢰할 수 있게 된다.