Things I can blog about

UTS vs UNSW vs USYD comp Sci + choosing a uni, factors to consider, my experiences
Why I code
Who am I
Teaching as a noble act
Picking a team work/uni

Type Theory Series

how it is useful
- what is a formal specification
- writing and verifying a formal specification (abstractly, what does it entail, what is a spec, what are requirements)
- proving leftpad- first spec then proof
- applications of this (hardware spec, nasa, idk look use cases up)
- ideally should finish the hott game before doing part 2 and 3 (need to know how modeling and non equal equivalences work)
- also HoTT book
- ideally even awodey cat theory book
what is HoTT (mathematical background for first HoTT program)
- "we are going to model homotopy theory"
- what is homotopy theory (continuous deformations, paths and loops in a topological space)
- spaces are types, terms are points in that space, equality is a path and there is a path space/identity type etc
- what does it mean for TT to model something (the problem with GTT)
- https://math.stackexchange.com/questions/3967700/in-what-sense-does-homotopy-type-theory-model-types-as-spaces
- what is univalence, infinity groupoids, why does HoTT work
- anything about denotational semantics would come here
- let us prove a result within it, some background
- what is a group
- what is the fundamental group of a space e.g. circle, sphere, torus
- conclude with "we are proving the fundamental group of S1 is isomoprhic to Z"
first HoTT program
- getting set up (instructions to install agda and cubical)
- the program: proving the fundamental group of S1 is isomoprhic to Z