Imagine if all the proofs in your linear algebra textbook were done in Isabelle, Idris or something similar to that. Then you'd be able to interactively explore

Imagine if all the proofs in your linear algebra textbook were done in Isabelle, Idris or something similar to that. Then you'd be able to interactively explore the proof, it would be unambiguous, and you would know exactly like it worked. If you don't understand how a C program generates its result, you could start a debugger and single-step through it. With a paper proof, how can you convince yourself that there is nothing missing in the proof? Maybe you think you understood, but you didn't.