The picture isn't quite so clean in the constructive context, which is what many of these proof systems are rooted in, e.g., https://mathoverflow.net/questions

The picture isn't quite so clean in the constructive context, which is what many of these proof systems are rooted in, e.g., https://mathoverflow.net/questions/236483/difference-between-constructive-dedekind-and-cauchy-reals-in-computation https://mathoverflow.net/questions/236483/difference-between...