[HN Gopher] Open Logic Project
       ___________________________________________________________________
        
       Open Logic Project
        
       Author : peanutcrisis
       Score  : 126 points
       Date   : 2022-07-02 16:12 UTC (6 hours ago)
        
 (HTM) web link (builds.openlogicproject.org)
 (TXT) w3m dump (builds.openlogicproject.org)
        
       | leeuw01 wrote:
       | Do these books also have an accompanying solution manual?
       | 
       | I couldn't find them on the website. I'd love to work my way
       | through these books. However, I'm afraid the reality will be that
       | I'll get stuck on solution, can't figure it out within an hour,
       | and lose motivation.
        
       | dang wrote:
       | Related:
       | 
       |  _Open Logic Project: An Open-Source, Collaborative Logic Text_ -
       | https://news.ycombinator.com/item?id=17739248 - Aug 2018 (8
       | comments)
       | 
       |  _The Open Logic Project_ -
       | https://news.ycombinator.com/item?id=9961863 - July 2015 (12
       | comments)
        
       | dennisy wrote:
       | I would be very interested to understand how people use logic
       | theories in day to day life or work?
       | 
       | Is this something which one can learn and use in other walks of
       | life, for example programming or ML?
       | 
       | Edit:
       | 
       | What I often find is that reading this type of material seems
       | very mentally stimulating, but these texts do not seem to offer
       | any introduction or intuition as to why someone should learn this
       | material or how to use it outside of the logic domain.
        
         | zozbot234 wrote:
         | It's more like a foundation for other types of material such as
         | the theory of programming languages (which helps in
         | understanding things like ML). Just about every paper or
         | textbook in PLT relies on logic-based notation and concepts.
        
         | tunesmith wrote:
         | Having a more grounded understanding of logic, even a 101-level
         | course understanding, can be really helpful in a technical job.
         | I think reviewing materials like these, in combination with a
         | basic understanding of Bayesian probability, has been very
         | helpful when acting as a team lead or cross-team architect with
         | my team of programmers.
         | 
         | It's ultimately stuff that feels obvious-in-hindsight and thus
         | easy to undervalue, but for me it encompasses matters such as:
         | 
         | 1) Making sure that a desired solution actually addresses an
         | explicitly understood problem (other than "the problem is that
         | the desired solution isn't in place!") This means being able to
         | explicitly state the problem and symptoms as a state of current
         | reality, separate from discussion of what the solution should
         | be.
         | 
         | 2) Resisting the urge to seize on the easiest-to-grasp
         | potential cause of an effect (this is a big one with many
         | programmers, I am constantly asking things like, "are you sure
         | that's the _only_ possible cause? " and "but if that were the
         | cause, wouldn't this _other_ effect, which is not happening,
         | also be happening? ") People can waste a lot of time chasing
         | theories that don't fully explain the symptoms.
         | 
         | 3) Constantly testing and updating mental models. For instance,
         | I am frequently urging team members to state their expectations
         | before running an experiment, rather than just "seeing what
         | happens". For example, "now that I have set this configuration
         | value, I expect to see this effect". This is to guard against
         | the "let's just hack until it seems to work" phenomenon, which
         | is a recipe for introducing latent bugs from not understanding
         | the whole system/model.
         | 
         | 4) Better communication! Engineers have a habit of speaking in
         | shorthand, causing other people to say, "Wait, can we back up a
         | bit?" (Or worse, not doing so when they should.) Explicitly
         | setting context up front, including explicitly stating
         | assumptions up front, better sets the table for group
         | discussions where everyone is on the same page. Under-
         | communicating is more frustrating than over-communicating.
         | 
         | 5) The final benefit of #4 is that if you are responsible about
         | stating the premises/assumptions that lead to your conclusion,
         | then you have effectively depersonalized the discussion. Such
         | that, if through discussion you discover that a
         | premise/assumption underlying a conclusion is incorrect, then
         | you can easily switch gears. Since the conclusion flowed from
         | that set of stated premises, rather than "Person X being
         | adamant", then it is easier that Premise #3 is wrong than
         | "Person X being wrong".
         | 
         | Anyway, all of these practices are easier to implement and
         | follow if you have an appreciation for the kinds of logical
         | concepts taught in basic logic courses.
        
           | dennisy wrote:
           | Thank you! That is extremely helpful.
        
           | jonsen wrote:
           | I definitely agree, but for your use cases wouldn't there be
           | more appropriate texts like for example _Meaning and
           | Argument_ :
           | 
           | https://www.amazon.com/Meaning-Argument-Introduction-
           | Through...
        
         | pron wrote:
         | I've used TLA+ extensively when designing distributed systems.
         | It's a mathematical logic language for describing systems and
         | verifying their properties.
        
         | deltaonefour wrote:
         | This stuff is foundational to things that check for program
         | correctness. For examples type checkers check if the program is
         | type correct. The foundations of these checkers rest on the
         | content of these pages.
         | 
         | It goes even further then this in the sense that with logic you
         | can design a language with correctness checking where even the
         | logic of your entire program can be verified via something
         | similar to a type check. So for example, Agda or Idris are
         | examples of languages with this capability.
         | 
         | So basically most of this stuff isn't relative to most job.
         | It's a higher level thing. It's more advanced theory for the
         | people who create the tools SO you can do your job. A step
         | above Dev Ops... it's the people who create the languages you
         | use.
        
         | [deleted]
        
       | jimhefferon wrote:
       | Has anyone here taught out of any of these, or tried working
       | through any of them? I'd be very interested in comments, general
       | or specific. (I am starting up a Logic class at my school.)
        
       ___________________________________________________________________
       (page generated 2022-07-02 23:00 UTC)