As far as I understand, Curry-Howard Correspondence is metaphorically a magical mirror which makes programming concepts and tricks be seen as mathematical theorem/proof elements and vice versa. Wikipedia even includes some table that maps items from programming world to mathematical world.

One of things, perception of which relatively has recently changed in programming world is Undefined Behaviour. From compiler's view, it is seen as a permit to do various transformations of the source code based on assumption that undefined behaviour never actually happens.

What is mathematician's analogue to programmer's Undefined Behaviour? Does it correspond to e.g. contradictions under Curry-Howard Isomorphism?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.