tag:blogger.com,1999:blog-5379029595723770792.post3314592420717502973..comments2022-04-08T08:41:45.591-07:00Comments on The Barbarian Programmer: Tactics will get you through times of no Strategy, better than Strategy will get you through times of no TacticsGregorhttp://www.blogger.com/profile/15214889337527469153noreply@blogger.comBlogger1125tag:blogger.com,1999:blog-5379029595723770792.post-24318114518287836742015-11-30T12:02:28.199-08:002015-11-30T12:02:28.199-08:00If you have done any proof using a proof assistant...If you have done any proof using a proof assistant, or any mathematical proof for that matter, you will relate to what I will share.<br /><br />In those proofs, we start with a general, high-level goal (strategy), and we use proof tactics towards that goal. It is actually called “tactics” in the Coq Proof Assistant. The strategy is generally vague, and the only clue suggesting that we should move in that direction is a “hunch” (or an “intuition” as most logicians would prefer here).<br /><br />While I was doing proofs for my thesis, I had times where I believed that my claims were true, but without well-defined mathematical tactics, I wouldn’t be able to reach the conclusion. And there were cases where I needed to change my overall goal based on the tactics I applied (e.g. seeing that there is a dead end in some part of my overall strategy). In other words, tactics showed me that I am in the wrong path. You can think of the feedback loop in "scientific method".<br /><br />As mentioned in your post, strategy keeps you in track, but without tactics, it doesn’t mean much. Tactical excellence is the best toolbox you would carry with you and context does not matter a lot, if you know how to use your tactics.Mustafa Zenginhttps://www.blogger.com/profile/06453260206161864294noreply@blogger.com