Writing modular programs in proof assistants is notoriously difficult. A significant literature and implementation effort is devoted to the topic, with approaches ranging from adding new constructions to the underlying logic, to adding features to the proof assistant. However, all current options (including records, sections and modules) are unsatisfactory in one way or another. In this work (in progress), we aim at reconciling the pros of several options using frames.