Sunday, 08/22/2021

GO HOMEEDIT

07:48 plmw notes

where do you want to make an impact?

ensuring learning

managing 'drinking from the firehose'

getting most ouf of your advior!

what do I want?

learning to use editors better

  1. add some keyboard shortcuts with semantic knowledge of the code

  2. write those shortcuts down on paper or in a document that will be readily available

  3. consciously practice them until they stick! i don't know enough of them yet.

metatheory

cannot pattern match on functino bodies in agdaa, ocaml - functions are 'black box'. must examine inputs and outputs contextual modal type theory: model context and holes in our language! give a hole a name: a contextual variable. can instantiate with a contextual texm, reifying LF typing derivations! build a proof system for manipulating these contextual objects - to get proofs as functional programs! abode the water, we have induction, case analysis, quantification; allowed to pattern match on contextual objects in beluga instead! write as recursive program; abstract over contexts, higher order pattern matching Learn more about Beluga! meta programming fox contextual types: allowing system f to match on itself. contextual types provide high level framework; broad, logical foundation for working with well scoped programs. learning theorem provieg: skills are transferable; just pick one to learn and roll with it! the most important thing, like all things, is to start - without starting nothing can be done.

emotional machines

turns out feelings are very important indications of what we want, need and believe in! we have certain biological needs and require emotional maintenance! mental health is fundamentally a social endeavor - talk to others!! get stuck in 'loops of distraction' instead of dealing with what you want do deal with; avoiding using whatever vice you have access to. unhealthy 'fawn response' - keeping safe through appeasing others. contrarily develops aversion to saying no and ending up deeply overcommitted to others! freeze response: procrastinate, isolate, withdraw, narrowing life, dissassociation; anything but engage with the topic that gives you this emotional struggle

tolerating your feelings: listen to all of them, then decide how to respond to them. making new choices than what we're comfortable with is profoundly difficult - but the more we resist our instant emotional responses, the better we can rationalize and make decisions that are better for ourselves. the first step to fixing these behaviors is identifying these behaviors and working on them, navigating those feelings and behaviors so that you become more accustomed to these healthy responses.

combining this with management and leadership roles: these things are even more important when you're responsible for others! cannot project your on feelings onto those you're trying to support!

writing papers

come back to this! talk and essay by derek dryer.

pl for expressing data structures!

abstraction to allow linking to single implementation of ADS, proven correct with a standard language toolkit contains a language extension or expressing these data structures, a type system, and a type safety guarantee that only a hash collision can invalidate the security of the data structure parsing away sql solutions for security

verifying data planes: network misconfiguration can make things unreachable, poorly route packets and decrease quaiytl of service p4: language for programming data planes on routers. verifying the p4 language

barriers to entry: PL expressive notation! difficult to understand and therefore use. need better education, tutorials, and other things (like distill.pub) and others. standardize notation! many use their own curtomized notation rather than a general one - still.

there are far more building builders than brickmakers; but this makes working in developer tools far more important. working on tools others use has this multiplicative, compounding factor; a compiler optimization optimizes every program written with that compiler! This power to have a disproportionate impact on programming and program development is incredibly valuable.

Teaching functional programming