By 'type concerns' i mean coercing the real world into the type system. You want that to be at the edge.

IMO, treating a program as a proof is somewhat impracticable as you see with very pure functional programming paradigms struggle with universal state monads.