How do you express computational content in non-constructive logic while both making it usable from proofs (e.g. if I have some algorithm that turns A's into B's, I want that to be directly referenceable in a proof - if A's have been posited, I must be able to turn them into B's) and keeping its character as specifically computational? Expressing algorithms in a totally separate way from proofs is arguably not much of a solution.