Frank's website

Hello, my name is Frank Dai. You've found my home site.

Here's a picture of me from March 2019.

A picture of me and Einstein being buds

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 Emoji: 🤔

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