[tom_mellior]

True, there are probably no theoretical obstacles. But there is a huge implementation effort, and judging from other new proof assistants that started out without tactics, I wouldn't hold my breath.

Unless you desperately need exactly this kind of fancy logic, if you actually want to get stuff done, you would choose a different system. That's not great if they are interested in wide adoption.