<b_jonas> learn Church invented a sane model of computation, but Turing was better with marketing, so now people define theoretical computer science using obsolate hardware like tape recorders.

The cut-elimination theorem states that any Prolog program written using the cut operator ! can be rewritten without using that operator.