Frank's website
Hello, my name is Frank Dai. You've found my home site.
Here's a picture of me from March 2019.
Contact
Anonymous contact/feedback form: Anonymous Feedback
Ymous Contact: Pick a unique identifier@fyd.ai
External Links
Blog: Doesn't exist yet, but eventually at blog.fyd.ai
Github: https://github.com/fydai (Note: personal projects are not public)
Twitter: No
LinkedIn: No
Instagram: No, but you can see my favorite sunset picture here.
Telegram: Exercise for reader
TikTok: Redacted as per Executive Order
About me
Age: 24
Location: Bay Area
Occupation: Undergraduate at UC Berkeley
Major: Math/Computer Science
Favorite Theorem: Bayes' Law
Interests
I like powerful abstractions. Ideas that make you say "of course that's how
things are, everything makes sense now". Ideas, which, after you learn them,
never leave you and stay with you forever. Here are some abstractions in
some topics I think about.
Type Theory
There is the Curry-Howard isomorphism, (or the nLab generalization of computational
trinitarianism), which says that logic and programming languages are the
same. Sometimes, I think about how to design better programming languages
keeping in mind the logic and the categories. I have nothing to show for this
thinking yet, but maybe one day I will. I'm not too happy with the state of type
theories at the moment. Universes I think are unnatural, mostly because it
forces upon you the travesty of universe polymorphism. I would prefer an
impredicative type theory, like the vanilla Calculus of Constructions, and
somehow add "inductive" there without incurring the wrath of universes. Of
course, everything should also be homotopic by default, or at the very least,
not exclude homotopy type theories.
Compilers
I have this philosophy that compilers are just (relatively) pure functions. It
takes some human written representation, and spits out output, which reality can
interpret as a function somehow. I imagine a very high level type-theory based
intermediate language, that you could compile existing languages to with a lot
of work, and build new languages around. From the intermediate language, you
could compile different parts of your program to various different backends. You
could draw a line in the program, say "this half runs on the server" and "this
half runs on the browser", and the compiler would just do the right thing
(dealing with the standard devops and webdev complexities for you). You could
say "do matrix operations on the GPU when it makes sense" and it would try its
best to determine when it makes sense.
State Management
Declarativity is the way of the future. I don't know why, but the second
infrastructure gets moved from "here's some scripts to move from state A to
state B" to "I'm describing state B, make it happen", something magical seems to
happen. I guess I stop thinking about the complexities of "what state is it in
right now", trusting that the software can get to state B from any state A. I've
realized that figuring out what the current state is, and considering all
possible things it could be, and how to deal with every possible
thing is horrible. We should have software like Kubernetes, but for all
possible state in the world, not just containers,
Interactive Theorem Proving
Hopefully I get to relabel this "automated theorem proving" eventually. After
doing a bit of interactive theorem proving, something in me hurts when I write a
paragraph proof. I need to constantly decide whether things obvious to me will
be obvious to the reader. There's also manual steps (infering the base/inductive
cases for instance) that I wish I could do with an "induction" tactic, but
instead I need to manually write them out. Sometimes I mix up two variables and
realize half an hour later of hair-pulling. Eventually I get better at these
things, but then again, a C programmer gets better at debugging segfaults. I
think we can do better. The best we've come is (in my opinion) Lean or Isabelle.
Lean is quite modern, but needs a lot of polishing and library effort. Using it
right now is an adventure into learning the hundreds of pitfalls in the tactic
library right now (like why are there things that dsimp
can simplify
but simp
can't). Isabelle with its sledgehammer
button
comes the closest to what I imagine interactive theorem proving could be. Write
a subgoal, and have the computer solve it with a 500 char-long auto
invocation. However, its theory is limited to first order logic, which heavily
restricts its usefulness.
Conclusion
If you want to contact me about any of these ideas, I would absolutely love to
talk to them. My contact information is all the way at the top of the page. If
you want to contact me for any other reason, you already know where my contact
information is.
Bye!
Last updated: October 2020