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.
TODO
Some observations on the situations of academic and industrial computer science -- as extremely general as the topic is.
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.
I recently contracted SARS-CoV-2. Here's my story.
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.
How can we expect expect mathematical explanations to manifest in real phenomenon in the actual world?
This is an example post to demonstrate Markdown features.
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?
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.
Some terms are uniquely (up to normalization and α-renaming) determined by their types.
Staring at a tree for one year.
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.
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 narrative demonstration of call-by-name's reflection of call-by-value in the dual calculus of Gentzen's sequential calculus.
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.
Is there generality to Descartes' personal recognition of the existing self?
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.
Were they special because they were mine?
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.
A day in the life of a student at a most practical university.
To survive guilt.
A proof that God cannot create a rock He cannot lift.
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.
This is an example to test backlinks.
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?
My essential mac applications that I always install right away.
What would different kinds of dimensional configurations, both spacial and temporal, appear like from an inside perspective?
The story of Aya Koike’s pursuit for love.
_
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.
A short exploration of how markets and planning shape cities.
How should the upsides and downsides of Democracy be weighted?
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.
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.
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?
An overview of different capabilities and styles of metaprogramming.
Do you choose to belief something, or do you recognize that you already believe it?
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 view of the epistomology of science centered around God.
I express my frustration with the current state of podcast-sharing capabilities, and outline what kinds of solutions I'd like to see.
Favor skepticism or pedagogy?
_
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?
Is it possible, and under what circumstances, for there to be no valid explanation of a phenomenon?
My thoughts on the dangers of AI technology.
Where do you go in cryostasis?
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.
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.
My middle and high school experiences were mainly boring, long, and inefficient. However, now everything has changed with the advent of personalized AI tutors.