Computing with excluded middle, like in Griffin's "A Formulae As Types Notion of Control"

Translated to OCaml using the double-negation translation of classical to intuitionist logic.

type void = |

type 'a not = 'a -> void
        
type 'a a_or_not_a =
    | A of  'a
    | Not_a of 'a not

let not_not_excluded_middle: type a. a a_or_not_a not not =
    fun k -> k (Not_a (fun (a: a): void -> k (A a)))

let rec loop_forever : unit -> void =
    fun () -> loop_forever ()

let use_excluded_middle: int a_or_not_a -> void = function
    | A a ->
            (* a is 3. We only got out what we put in. And now we have to return void *)
            loop_forever ()
    | Not_a f -> f 3

(* of course, loops forever*)
let _: void = not_not_excluded_middle use_excluded_middle

It's the "Devil's Bargain" from Wadler's "Call-by-Value is Dual to Call-by-Name": an apparently-useless stunt.

But, theoretically, there are several ways of using excluded middle to compute interesting things:

Backtracking– .... no reference found Using classical linear logic as a high-level language compilable to intuitionist logic. Haven't found programming use cases yet, but there are examples in Shulman's "Affine logic for constructive mathematics"