Yea and I consider dependent types to be a false idol for the reasons I outlined before. Eventually you just need to compute an arbitrary program within a type

Yea and I consider dependent types to be a false idol for the reasons I outlined before. Eventually you just need to compute an arbitrary program within a type check, which is equivalent to just executing the program to begin with.