If you mean that implementing the LCF architecture OP advocates for or evaluating any one implementation of it for soundness isn't easy, I absolutely agree. But assuming that you've solved that part, making use of it within a system that otherwise uses dependent types is not that hard.
If you mean that implementing the LCF architecture OP advocates for or evaluating any one implementation of it for soundness isn't easy, I absolutely agree. But assuming that you've solved that part, making use of it within a system that otherwise uses dependent types is not that hard.