 Another objection to the theoretical possibility of mathematical correctness is that since proofs are carried out by a theorem prover, i.e. a physical machine, the knowledge one attains about computational systems is not a-priori but empirical (see Turner 2018 ch. 25). However, Burge (1988) argues that computer-based proofs of correctness can still be regarded as a-priori, in that even though their possibility depends on sensory experience, their justification does not (as it is for a-posteriori knowledge). For instance, the knowledge that red is a color is a-priori even though it requires having sensory experience of red; this is because ‘red is a colour’ is true independently of any sensory experience. For further discussion on the nature of the use of computers in mathematical proofs, see (Hales 2008; Harrison 2008; Tymoczko 1979, 1980).