I am currently hold a Sapere Aude grant for a project funded by the Danish Ministry of Science. The scope of this project is twofold. First of all we aim to provide an environment where researchers can prototype new programming languages and specification logics and prove that programs are correct with respect to their specifications inside the interactive proof asssistant Coq. Secondly, we will provide an Eclipse perspective that extends the current Java perspective of Eclipse allowing users to verify the correctness of Java programs in the same environment as in which they write their programs. For more information, see the project homepage.