The essence of CH is "proofs = programs" and "program execution = cut elimination". As far as I understand this does not work precisely as of Jan 2017 for most

The essence of CH is "proofs = programs" and "program execution = cut elimination". As far as I understand this does not work precisely as of Jan 2017 for most forms of computation beyond strongly normalising pure functions. If you are broadening what you mean by CH, then fair enough, but it's shifting the argument.