"Proofs via computations" by now is an established method within Computer Mathematics. The converse, computations via proofs, has as aim to use a (constructive or classical) proof as an algorithm, whenever possible. Both theoretical and practical aspects will be presented. Recent work of Cruz-Filippe and Spitters shows that there is space for improvements in efficiency.