Index

Using Agda Macros as Interactive Tactics

Published: 2025-05-13

Tags: computics, Agda

Abstract

A proposal for how to use Agda's macro capabilities to emulate the features of interactive tactics LTac in Coq/Rocq. Agda's typed holes already get almost all the way there; they just need to handle interactive holes well!

Meritocracy is wrong

Published: 2024-06-23

Tags: philosophy

Review of the Arc Browser

Published: 2024-03-05

Tags: technology

Abstract

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.

Open Source Software

Published: 2023-11-11

Tags: technology, software

Abstract

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.

Aligned Intelligence and Moral Progress

Published: 2023-06-06

Tags: philosophy, ai

Abstract

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?

The Next Trillion Theorems

Published: 2023-05-05

Tags: mathematics, ai

Abstract

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?

AI Tutors – The Future of Education

Published: 2023-05-05

Tags: ai, education

Abstract

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

AI Danger

Published: 2023-04-03

Tags: ai

Abstract

My thoughts on the dangers of AI technology.

Essential Mac Applications

Published: 2022-11-27

Tags: technology, software

Abstract

My essential mac applications that I always install right away.

Rumble VR

Published: 2022-11-25

Tags: vr, technology, game

Abstract

My review of the Rumble VR videogame.

Social VR?

Published: 2022-10-22

Tags: technology, vr

Abstract

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

Metaprogramming Capabilities

Published: 2022-09-27

Tags: computics, Haskell

Abstract

An overview of different capabilities and styles of metaprogramming.

agda2lh

Published: 2022-09-17

Tags: computics, Agda, Haskell, LiquidHaskell

Abstract

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.

The Situations of Academic and Industrial Computer Science

Published: 2022-09-09

Tags: computics, academia

Abstract

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

Love Exposure

Published: 2022-08-17

Tags: movie, short-story

Abstract

The story of Aya Koike’s pursuit for love.

My Experience with the Great SARS-CoV-2 Virus

Published: 2022-06-20

Tags: biography

Abstract

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

Kelvin Versioning

Published: 2022-06-08

Tags: software-engineering

Abstract

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.

Forgiving US Student Loan Debt

Published: 2022-04-17

Tags: academics, economics

Abstract

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.

Reflections on Academic Conferences

Published: 2022-01-28

Tags: academics

Abstract

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?

Overloaded Functions in Haskell

Published: 2021-11-07

Tags: computics, Haskell

Abstract

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).

Is Belief a Choice?

Published: 2021-11-01

Tags: philosophy

Abstract

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

The Difference Between Mathematics and Logic

Published: 2021-10-17

Tags: computics, philosophy, mathematics

Abstract

What is the difference between mathematics and logic?

Unique Terms

Published: 2021-09-01

Tags: computics

Abstract

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

Cryodreams

Published: 2021-08-29

Tags: philosophy, technology, short-story

Abstract

Where do you go in cryostasis?

A Proof That God Cannot Create a Rock So Heavy He Cannot Lift It

Published: 2021-08-26

Tags: philosophy

Abstract

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

Competiting with YouTube

Published: 2021-08-25

Tags: technology

Abstract

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?

Metaprogramming via Dependent Types

Published: 2021-08-24

Tags: computics

Abstract

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 Monotheistic Foundation for the Epistemology of Science

Published: 2021-08-24

Tags: philosophy, science

Abstract

A view of the epistomology of science centered around God.

Mesaprogramming

Published: 2021-08-24

Tags: computics

Abstract

Reminders

Published: 2021-08-20

Tags: short-story

Abstract

A short story.

Losing Touch

Published: 2021-08-14

Tags: short-story

Abstract

A short story.

Moral Empiricism

Published: 2021-07-29

Tags: philosophy

Abstract

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.

Strategy Games are Puzzle Games with Computational Constraints

Published: 2021-06-10

Tags:

Abstract

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.

From Inside Dimensions

Published: 2021-05-29

Tags: theoretical-physics, mathematics

Abstract

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

An Analogy is Like a Bad Argument

Published: 2021-04-25

Tags: writing

Abstract

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.

Types of "Type"s

Published: 2021-04-15

Tags: computics

Abstract

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.

Placebo Discount

Published: 2021-03-28

Tags: economics, medicine

Abstract

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.

Impe

Published: 2021-03-15

Tags: computics, Haskell

Abstract

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.

Magic the Gathering - Deckbuilder Draft

Published: 2021-01-08

Tags: game-design

Abstract

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.

Augmentation 1

Published: 2021-01-07

Tags: short-story

Abstract

Were they special because they were mine?

The Social Responsibility of Business in "A Friedman Doctrine"

Published: 2020-11-28

Tags: economics, ethics

Abstract

My thoughts on "A Friedman Doctrine".

Dominant Assurance Contracts

Published: 2020-11-10

Tags: economics

Abstract

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.