what if heat, but plate

\begin{equation} \pdv{u}{t} = \pdv[2]{u}{x} + \pdv[2]{u}{y} \end{equation}

For some heat distribution that has arbitrary shape, on some domain \(\Omega \times [0, \infty]_{t}\) (i.e. argumentation of some space dimensions by time).

• Dirichlet Conditions: edges have heat \(0\)
• OR Neumann Conditions: normal derivative (flux) is \(0\) at the edge

If \(\Omega\) is a general blob, you are actually kinda fucked. Because the bounds on \(x\) depend on \(y\), and \(y\) on \(x\), so you can’t just separate them into a product.

Say we want to find the number which is the additive inverse (“negative”) of a number.

We can just flip each of the digit, and then add 1:

• take \(0101\), invert it to get \(1010\)
• adding these two numbers will give you \(1111\). If we just added one more \(0001\), it will flip over to be \(0000\).
• Therefore, \(1010+0001 = 1011\) is the additive inverse of \(0101\).

The left most bit being one: still a mark of whether or not something is negative. It just works backwards:

type theory was originally aimed creating a basis of all of mathematics. it got out-competed in math by set theory. it formalizes…

1. programs
2. propositions (types)
3. proofs that programs satisfies these propositions

and does so in one system.

key features

• it creates an isomorphism between programs/types with proofs/propositions
• it creates a hierarchy which allows defining types, type operations, proofs into the same system at different levels
• it allows possibly-undecidable expressive dependent types to be constructed

musing

• this is a foundation of mathematics, and in particular constructive mathematics
• its pretty powerful to prove anything we want to prove—so can be used to verify the correctness of all sofware

properties of type systems

type stratification

Consider a type of all types Type,

• quality of service harm
• distributive harm
• existential harm

what is a type? a type is a set of values.

consider

List[Int]; importantly, List is not a type; its a “type constructor” which takes a type as input (Int) and gives you as type as output List[int].

-> is another “type constructor”; its a type constructor written in infix notation. It takes two arguments, it constructs a type for set of functions which takes an integer as input and maps it to another integer Int -> Int