This paper shows that synthesizing binary decision programs (formed by means of decision instructions of the type ''if then else'' and of execution instructions of the type ''do'') and proving theorems can be carried out by using the same approach. It is proved that the same transformations acting on P-functions can be interpreted in terms of binary program synthesis and of theorem proving. Since binary program leads to algorithmic state machine design while theorem proving leads to declarative programming, this allows us to lay a bridge between logic design and declarative languages such as Prolog.