Some 25 years ago Martin-Loef pointed out a close connection between constructive mathematics and computer programming. There is now some interest in this idea. But what about input output? What should be the interface of a dependently typed programming language to the real world? I came across an elegant data structure devised by Petersson and Synek that seems to offer one approach, and have developed it in collaboration with Anton Setzer and Pierre Hyvernat. I'll try to motivate this approach, and indicate some of the developments.