My personal review of the Arc Browser, as someone who previously mainly used Safari and Firefox. Overall, I find Arc to provide a large number of unique improvements in the browsing experience, with only a few demerits.

My thoughts on open source software (OSS), in particular, the theoretical benefits of OSS, the practical shortcomings of OSS, and how to make a profitable company that writes (a nonnegligible amount of) OSS.

Why does it appear to us that history proceeds in a rough trend of "moral progress" with a peak in the recent past or current?

Fields such as theoretical computer science and mathematics are game-like and full of low-hanging fruit of unclear value. Could recently-developed AI technology harvest a bounty?

My middle and high school experiences were mainly boring, long, and inefficient. However, now everything has changed with the advent of **personalized** AI tutors.

My thoughts on the dangers of AI technology.

My essential mac applications that I always install right away.

Review of the Rumble VR videogame.

What's involved in being social in VR? How does it compare to real life? A case study with VRChat and RecRoom.

An overview of different capabilities and styles of metaprogramming.

The project `agda2hs` claims that a reasonable subset of Agda programs can be directly compiled to Haskell programs which can be considered verified up to the Agda programs' specifications. However, `agda2hs`'s extraction leaves the resulting Haskell program bare of all statically-checkable guarantees from the perspective of client Haskell programs that would like to use it. This article proposes a modified extraction `agda2lh` which compiles a reasonable Agda program, which has specifications in terms of decidable relations, to a Liquid Haskell program that includes those specifications as Liquid Haskell refinements. Such a Liquid Haskell program exposes the Agda-originating specifications to client Haskell code that also uses Liquid Haskell to variable degree.

Some observations on the situations of academic and industrial computer science -- as extremely general as the topic is.

The story of Aya Koike’s pursuit for love.

I recently contracted SARS-CoV-2. Here's my story.

Kelvin versioning is an uncommon versioning scheme, introduced by Curtis Yarvin at Urbit, that enumerates newer versions with lower natural numbers. When version 0K is reached, no more changes are allowed -- this final version is, permanently, "frozen". I present a way to arrive at versioning schemes like semantic versioning (semver) and Kelvin versioning (kelver) from first principles, and propose an variant of Kelvin versioning that mirrors the way that semantic versioning improved upon more primitive versioning schemes.

Over the last 18 years, student loan debt has increased 28% -- from $0.49 trillion (not 2021-inflation adjusted as $0.33 trillion) in 2003 to $1.75 trillion in 2021. And there are increases of similar magnitudes of the number of students taking on debt. There have been many popular calls for the government help students with this debt, especially since 92.6% of the current outstanding student loan debt is borrowed from the federal government.

Academic conferences are large formal gatherings where researchers in a particular field share their refereed results in the form of talks and workshops. What are the goals of such conferences, and how well do they achieve them in practice?

TODO

Basic Haskell functions do not support overloading, which is a feature that allows for multiple terms to have the same name in the same scope. This post demonstrates a comparison between three approaches to implementing overloading in Haskell -- typeclasses, templates, and singletons (mesaprogramming).

Do you choose to belief something, or do you recognize that you already believe it?

What is the difference between mathematics and logic?

Some terms are uniquely (up to normalization and α-renaming) determined by their types.

Where do you go in cryostasis?

A proof that God cannot create a rock He cannot lift.

YouTube is hugely dominant in the market of general public video hosting. Why is YouTube so dominant, how should new competators take on YouTube, and will YouTube maintain its dominance over the next 10 years?

In general, metaprogramming is implemented in a type-unsafe way i.e. it ignores type information in generated code. This is often considered satisfactory since type-checking is still performed at compile-time, so code generation cannot introduce new runtime errors that would be caught at compile-time by type-checking the generated code. However, a type-safe approach offers a much more robust way to provide expressive metaprogramming capabilities in a way that naturally parallels the use of the base language. For example. this approach extends naturally to safe tactics.

A view of the epistomology of science centered around God.

In general, metaprogramming is implemented in a type-unsafe way i.e. it ignores type information in generated code. This is often considered satisfactory since type-checking is still performed at compile-time, so code generation cannot introduce new runtime errors that would be caught at compile-time by type-checking the generated code. However, a type-safe approach offers a much more robust way to provide expressive metaprogramming capabilities in a way that naturally parallels the use of the base language. For example. this approach extends naturally to safe tactics.

_

_

What are the consequences of the view that moral truths are empirical truths about human nature i.e. derivable empirically by studying human nature and behavior.

Even though strategy games often have solutions -- that is, perfect strategies -- the fact that players are computationally constrained from using the solution strategies makes strategy games different from puzzles.

What would different kinds of dimensional configurations, both spacial and temporal, appear like from an inside perspective?

Analogies are easily misused, with great effectiveness, as if they are arguments or explanations. Still, analogies can be used well to make a claim intuitive after it has been justified.

In mathematics and theoretical computer science, theoreticians seem to always be grasping for synonyms of the word "type." This post serves as a convenient resource for these words.

A proposal to monitize the placebo effect by selling, at a discount, bundles of doses of an effective drug that includes a certain percentage of placebo doses.

An explanation of NFTs. Some current use cases of NFTs. How NFTs can have value. Some future use cases for NFTs.

This is a demonstration of the design and implementation of a very simple imperative programming language, Impe, using Haskell. The goal is to demonstrate the convenience and advanced features and libraries that Haskell offers for programming language implementation.

A popular way to play Magic the Gathering is via a draft where players select cards to build decks, then compete in a small tournament with those decks. This article presents a modification of the typical draft format that incorporates deckbuilding from randomized markets between the tournament games, so that decks get progressively stronger and more specialized in a fair way throughout the tournament.

Were they special because they were mine?

TODO

The power of being a bad communicator.

Dominant assurance contracts are an interesting solution to many collective action problems. A DAC asks an agent to pledge a donation towards a collective action to be paid if any only if enough other agents also pledge, and promises to pay the agent if not enough other agents pledge. Such a contract can yield opting-in as a dominant strategy even when an agent expects other agents not to opt-in; free-rider incentives are removed by the assurance that no one benefits if any agent opts-out, and payment incentivizes pessimistic agents to opt-in anyway.

A narrative demonstration of call-by-name's reflection of call-by-value in the dual calculus of Gentzen's sequential calculus.

A day in the life of a student at a most practical university.

Staring at a tree for one year.

Is there generality to Descartes' personal recognition of the existing self?

How can we expect expect mathematical explanations to manifest in real phenomenon in the actual world?

How solid is the value inflating Bitcoin?

Is it possible, and under what circumstances, for there to be no valid explanation of a phenomenon?

I express my frustration with the current state of podcast-sharing capabilities, and outline what kinds of solutions I'd like to see.

How should the upsides and downsides of Democracy be weighted?

A short exploration of how markets and planning shape cities.

Favor skepticism or pedagogy?

To survive guilt.