&gt; This isn&#x27;t about motivation. Its not even about study, rather how do you go about doing formal reasoning at all? Prove X has property P, what is even the first step? How do we get to the second step, and so on? Doing a proof is not a mechanical process, there isn&#x27;t an algorithm for deciding what to do next to reach your goal!<p>Yep, there&#x27;s no general algorithm for coming up with proofs. Practice, experience and good heuristics help, though. And if they don&#x27;t, then you redesign the formal system until they do.<p>&gt; Programming is a great example of this. Those lists and arrays don&#x27;t appear out of nowhere. Someone has to write the code, how do they write the code?<p>Same as above. Just replace “proofs” with “programs”, and “formal system” with “programming language”.<p>&gt; Why use a list to store those elements?<p>The desired invariants (see below) and complexity bounds for your code will tell you what data structures might be more convenient than others.<p>&gt; Programs are generalized to operate on a wide variety of inputs to create a wide variety of outputs, but when you are writing code, you are thinking about just a few examples of those, you imagine them in your head and they guide the code you write.<p>I can&#x27;t speak for others, but I really don&#x27;t think that way. When I&#x27;m designing an algorithm, or when I&#x27;m trying to understand someone else&#x27;s design, what matters to me first and foremost is its <i>invariants</i> - what the program <i>preserves</i>, even though the process&#x27; state is changing. Only if I can&#x27;t see what the invariants are, then I might use some examples to generate plausible candidates, but the job isn&#x27;t done until I have found and confirmed the invariants themselves. In other words, I don&#x27;t conflate “works for these few examples” with “works in general”.