[neel_k]

You almost certainly have had to debug a Gödelian paradox in your day-to-day programming. It's just that programmers call it "nontermination" or "infinite loops".

In 1952 the logician Martin Löb invented something called "provability logic" as a way to formulate Gödel's theorem more abstractly, so that we could see how the proof worked without having to work with explicit numerical encodings of formulas. (Think of this as the difference between working with strings versus abstract syntax trees.)

His version of the proof is now called Löb's theorem, and its structure is almost identical to what logicians call Curry's paradox, and which (via the Curry-Howard correspondence) programmers know as the Y combinator. The Y combinator is used to implement recursion in the lambda calculus, specifically including the ability to go into infinite loops.

I blogged about this last year:

http://semantic-domain.blogspot.co.uk/2016/05/lobs-theorem-i...