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.

Interactive tactics, such as LTac in Coq/Rocq, support an interesting and often useful workflow: to interactively run a tactic script (which can leverage metaprogramming), viewing the context and expected type of the rest of the tactic script (in a nested fashion) at each step. In this way, you as a programmer can view the intermediate states that are yielded by metaprogrammatic computations which would otherwise be inaccessible if you were only able to view the final output of the tactic script.

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.

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

An overview of different capabilities and styles of metaprogramming.

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.

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.

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?

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.

TODO

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?

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?

My thoughts on the dangers of AI technology.

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

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

How solid is the value inflating Bitcoin?

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.

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.

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

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

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.

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

What is the difference between mathematics and logic?

An overview of different capabilities and styles of metaprogramming.

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.

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.

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

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

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.

TODO

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

TODO

This is an example post to demonstrate Markdown features.

This is an example to test backlinks.

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.

Interactive tactics, such as LTac in Coq/Rocq, support an interesting and often useful workflow: to interactively run a tactic script (which can leverage metaprogramming), viewing the context and expected type of the rest of the tactic script (in a nested fashion) at each step. In this way, you as a programmer can view the intermediate states that are yielded by metaprogrammatic computations which would otherwise be inaccessible if you were only able to view the final output of the tactic script.

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

What is the difference between mathematics and logic?

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

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?

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.

The story of Aya Koike’s pursuit for love.

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

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.

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

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

What is the difference between mathematics and logic?

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

A view of the epistomology of science centered around God.

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?

Where do you go in cryostasis?

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

A view of the epistomology of science centered around God.

Staring at a tree for one year.

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

Were they special because they were mine?

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

The story of Aya Koike’s pursuit for love.

_

_

Where do you go in cryostasis?

TODO

My essential mac applications that I always install right away.

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.

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.

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.

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

My essential mac applications that I always install right away.

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.

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?

How solid is the value inflating Bitcoin?

Where do you go in cryostasis?

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

Interactive tactics, such as LTac in Coq/Rocq, support an interesting and often useful workflow: to interactively run a tactic script (which can leverage metaprogramming), viewing the context and expected type of the rest of the tactic script (in a nested fashion) at each step. In this way, you as a programmer can view the intermediate states that are yielded by metaprogrammatic computations which would otherwise be inaccessible if you were only able to view the final output of the tactic script.

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

Review of the Rumble VR videogame.

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.