


# Boolean Considered Harmful

I make the claim that using the boolean type (called "Boolean")
is always a bad design decesion. This is because `Boolean` is
like the rind of an orange that has been squeezed out. The rind
testifies that there once was an orange here, but the juicy goodness
of the orange is long gone.

It is the same with `Boolean`. If you are using `Boolean`, there was
once a function which returned more information, but this helpful information
was thrown away when all the information was squashed down into only 2 states.

My recommendation is that for any time you are tempted to write "Boolean", consider
what information the function is actually computing.

To illustrate my point more, I will code the equality function on natural numbers in
[Agda](https://en.wikipedia.org/wiki/Agda_(programming_language)). For any natural numbers `x` and `y`, `x == y` returns `true` if `x` is equal
to `y` and false otherwise. I will then contrast this function against `x ==? y`, which I claim
is a better function.

Do not worry if you do not know [Agda](https://en.wikipedia.org/wiki/Agda_(programming_language)), because
I will be explaining the code at every step.


# Standard Library Functions

First, I will defining some standard functions.
These functions are all in the [standard library of Agda](https://agda.github.io/agda-stdlib/),
so this section is a learning exercise where I will be thouroughly explaining the purpose of all
the code.

## Peano Numbers

We will represent natural numbers as [Peano Numbers](https://en.wikipedia.org/wiki/Peano_axioms), which means
that every natural number is either `0` or `successor(n)` for some natural number `n`. In Agda, we would
represent the natural numbers as this data type:

```agda
data NaturalNumber : Set where
  zero : NaturalNumber
  successor : NaturalNumber → NaturalNumber
variable
  m n : NaturalNumber
```
## Booleans

We can then define the much-dreaded `Boolean`, which is either `true` or `false`.

```agda
data Boolean : Set where
  true : Boolean
  false : Boolean
```
## Booleanean (Bad) Equality

In our first attempt to define equality on natural numbers, we use a `Boolean` to represent the result:
`true` if the two numbers are equal and `false` if the two numbers are not equal.

```agda
infixr 5 _==_
_==_ : NaturalNumber → NaturalNumber → Boolean
zero == zero = true
successor a == zero = false
zero == successor b = false
successor a == successor b = a == b
```

## Propositional Equality

To begin to define our better equality, we first need a specification of equality.
Some beginners are confused by propositional equality because propositional equality
does not *compute* if two values are equal, but rather it gives the type of all *proofs*
that they are equal.

```agda
infixr 5 _≡_
data _≡_  {A : Set o} :  A → A →  Set (lsuc o) where
  reflexivity : {a : A} →  a ≡ a
```

So, for example, `a ≡ b` is the type of all proofs that `a` is equal to `b`.

## Empty Type

The empty type is inhabited by no values. The empty type represents the false proposition, or the proposition
with no proofs.

```agda
data empty : Set where
```

## Decidability

With these pieces, we can define `decidability`. A proposition
is [decidable](https://en.wikipedia.org/wiki/Decidability_(logic)) if there exists an
algorithm for deciding if the proposition is inhabited.
The `decides A` type will either produce evidence that `A` is inhabited, or
produce evidence that `A` in uninhabited.

```agda
data decides (A : Set o) : Set o where
  trueBecauseOf : A → decides A
  falseBecauseOf : (A → empty) → decides A
```

A simple utility function which proves that `successor` is
an [injective function](https://en.wikipedia.org/wiki/Injective_function).

```agda
successorInjective : successor m ≡ successor n → m ≡ n
successorInjective reflexivity = reflexivity
```

Given the type `decides`, we can say what it means for a [binary function](https://en.wikipedia.org/wiki/Binary_operation)
to be decidable: for all its inputs, we can produce evidence of the type
being inhabited or uninhabited.

```agda
decidable2 : {A B : Set o} →  (A → B → Set ℓ) → Set (o ⊔ ℓ)
decidable2 {A = A} {B = B} f = (a : A) (b : B) → decides (f a b)
```

# The Improved Natural Number Equality

We will now define the improved equality function on natural numbers:

```agda
infixr 5 _==?_
_==?_ : decidable2 {A = NaturalNumber}  (_≡_)
zero ==? zero = trueBecauseOf reflexivity
zero ==? successor y = falseBecauseOf λ ()
successor x ==? zero = falseBecauseOf λ ()
successor x ==? successor y with (x ==? y)
... | trueBecauseOf reflexivity = trueBecauseOf reflexivity
... | falseBecauseOf x≢y = falseBecauseOf  (λ z → x≢y (successorInjective z))
```

# Why the Deciding Verison is Better

You might be wondering: "why is `x ==? y` better than `x == y`". In short, it is because
`x ==? y` has a specification, but `x == y` does not.

What's more, for all inputs, `x ==? y` returns evidence that it is correct, whereas we have not even
stated the correctness specification for `x == y`.

You should always assume that everything is wrong until you have a formal proof that it is correct.

Any function with the type signature `decidable2 {A = NaturalNumber}  (_≡_)` *must* be correct. By
using a more expressive type, we have ensured correctness automatically.  Others have said
["make illegal states unrepresentable"](https://fsharpforfunandprofit.com/posts/designing-with-types-making-illegal-states-unrepresentable/)
but I say, "make incorrect code unwritable".
Write a specification so that the only option is for your code to be correct.

With the pedestrian `x == y`, it would be easy to write a function with the same type signature that,
in fact, would be incorrect.

The main concern in software is proofs of correctness. Every other aspect of code (including performance)
is secondary. To learn more about this, look at [this talk](https://github.com/conal/talk-2023-galilean-revolution).

For these reasons, I strongly advise that 90% of the use of `Boolean`s is incorrect, and could be
replaced by more informative types.


Boolean Considered Harmful




# What is an RSS Feed

RSS is a standard by which you may subscribe to the content of other websites, and recieve updates about the news on other websites in a 
standardized way so that many programs can read and understand the infromation. RSS uses XML in order to communicate in a way
that can be easily parsed by other tools and applications.

# RSS increases freedom and independence

My main promotion of RSS is a philosophical and ideological reason: RSS feeds increse freedom, independence, and decentralization on the internet.
Too often, the web has been centralized under the lock-and-key of a few gatekeepers (to name them: Google, Meta, Apple, Microsoft).
At the click of their fingers, and for whatever whim, as arbitrary as they desire, your subscriptions would be deleted without
any trace or recourse.

RSS feeds put the responsability in the hands of small website owners and blogs: because the standard is so simple, anyone
can implement and use it without the approval of those lords of the internet.

# How to Find RSS Feeds

Unfortunately for my idealistic ambitions, it seems that it is rare to find RSS feeds for the websites and information that I want.

What I usually do is open the devtools and search for "rss" or "atom" in the HTML.


## Tools for RSS

If my techniques don't work, sometimes there are tools out there to help you get an rss feed from a website.

One example is [Kill the Newsletter!](https://kill-the-newsletter.com/), which allows you to turn an email list into an
RSS feed.



# My RSS Config

For Edifying purposes, I will share my RSS configuration for others who want to take the first step into the world of RSS.
I use a program called [elfeed](https://github.com/skeeto/elfeed) as an RSS reader. Here is my configuration for elfeed.

```emacs-lisp
(setq elfeed-feeds
      '(
        ("https://www.unison-lang.org/feed.xml" unison programming-language)
        ("http://arxiv.org/rss/cs.LO" logic)
        ("http://arxiv.org/rss/cs.MS" math)
        ("http://arxiv.org/rss/cs.PL" programming-language)
        ("http://arxiv.org/rss/math.CT" category-theory)
        ("https://reddit.com/r/emacs.rss" emacs)
        ("https://reddit.com/r/orgmode.rss" emacs org-mode)
        ("https://reddit.com/r/nixOS.rss" nix linux)
        ("https://golem.ph.utexas.edu/category/atom10.xml" category-theory)
        ("https://hnrss.org/newest?points=20")
        ("https://lukesmith.xyz/index.xml")
        ("https://nyxt.atlas.engineer/feed")
        ("https://homotopytypetheory.org/feed/" homotopy-type-theory)
        ("https://math.andrej.com/feed.xml")
        ("https://existentialtype.wordpress.com/feed/" type-theory)
        ("https://blog.thjread.com/rss.xml")
        ("https://nitter.unixfox.eu/conal/rss")
        ("https://www.youtube.com/feeds/videos.xml?channel_id=UCS4FAVeYW_IaZqAbqhlvxlA" programming-language)
        ("https://www.youtube.com/feeds/videos.xml?channel_id=UC1kBxkk2bcG78YBX7LMl9pQ" programming-language)
        ("https://www.youtube.com/feeds/videos.xml?channel_id=UC-9jDbJ-HegCFuWuam1SfvQ" programming-language)
        ("https://www.youtube.com/feeds/videos.xml?channel_id=UCFFeNyzCEQDS4KCecugmotg" programming-language)
        ("https://hnrss.org/newest?q=linux&points=20" linux)
        ("https://hnrss.org/newest?q=type%20theory" type-theory)
        ("https://hnrss.org/newest?q=category%20theory" category-theory)
        ("https://nixos.org/blog/announcements-rss.xml" nix linux)
        ("https://github.com/AtticusKuhn.private.atom")
        ("https://feeds.buzzsprout.com/728558.rss" type-theory)
        ("https://blog.wolfram.com/feed/" wolfram programming-language)
        ("https://www.google.com/alerts/feeds/04747069146194916248/458592335938245591" type-theory)
        ("https://www.google.com/alerts/feeds/04747069146194916248/4667516096121066180" category-theory)
        ("https://www.google.com/alerts/feeds/04747069146194916248/7476438073175009204" homotopy-type-theory)
        ("https://nitter.unixfox.eu/ttforall/rss" type-theory)
        ("https://nitter.unixfox.eu/typetheorypcast/rss" type-theory)
        ("https://nitter.unixfox.eu/SydneyTypes/rss" type-theory)
        ("https://nitter.unixfox.eu/type_theory/with_replies/rss" type-theory)
        ("https://twitter.com/Jose_A_Alonso/with_replies" math type-theory)
        ("https://nitter.unixfox.eu/LogicPractice/rss" logic)
        ("https://www.johndcook.com/blog/feed/")
        ("https://systemcrafters.net/rss/" emacs)
        ("https://emacstil.com/feed.xml" emacs)
        ("https://d12frosted.io/atom.xml" emacs)
        ))
```

# My RSS Feed

Now that you are convinced of the benefits of using RSS, now would be a good time to mention that I have my own RSS feed. You can access my
RSS feed at [/rss.xml](/rss.xml)


Why RSS Feeds are the Superior way to Stay Up-to-Date



# Linux

I recently began to experiment with trying Linux, a free and open source operating system. I am a supporter
of open-source software because I believe that it gives us true control over what we do on our electronic
devices. 

# Nixos

For my first foray into the wild world of Linux, I decided to try Nixos because I think the philosophy
of everything being in 1 config file is pretty interesting. 


# My Experience

For the first few days, I couldn't get the X11 server to start and I was stuck in the TTY. I eventually
figured out that it was an issue with Intel Graphics, so I fixed it.

My experience was a bit slow and clunky starting out, but eventually, I became faster after I'd learning
all the tricks of the new software. I actually think I am faster and more efficient now because open-source
software tends to follow the Unix Philosophy of being modular and also has lots of modes and keybindings
to speed things up. 

# Software I've used

The thing I like most about free software is that it seems such software gives ultimate control and
customizability to the user. Here are the software packages that I am using right now, which I believe
grant the user ultimate control

* Nixos
* Emacs
* Xmonad / Xmobar

I'm looking for a new terminal to use. Right now I'm using Xterm, which isn't very good. If you have any
recommendations of terminals that I should try, you can contact me.


# My Configuration

If you want to see what configuration and dotfiles I'm using, go to my github because I have posted
my dotfiles and configuration files there. 



I recently switched to using only Linux. See how it turned out!

My experience using Linux




I recently looked at [A Talk by Bob Martin](https://www.youtube.com/watch?v=P2yr-3F6PQo) in which
he says that we've "basically discovered all the programming paradigms". He says this due to his
view that programming paradigms are just restrictions on what programmers can do, but I disagree.
My view is that **a good programming language is the minimal amount needed to add to a model
of computation**. I will explain what I mean.

## Models of Computation
According to Wikipedia, a [Model of Computation](https://en.wikipedia.org/wiki/Model_of_computation) is
"a model which describes how an output of a mathematical function is computed given an input".
There are a list of models of computation on the page, which include
- Post machines
- Pushdown automata
- Register machines
- Random-access machines
- Turing machines
- Decision tree model
- Abstract rewriting systems
- Combinatory logic
- General recursive functions
- Lambda calculus
- Actor model
- Cellular automaton
- Interaction nets
- Kahn process networks
- Logic gates and digital circuits
- Petri nets
- Synchronous Data Flow

As you can see, there are many models of computation.
## Minimal Addition
What do I mean by "minimal additon". Well, a model of computation only describes mathematical functions, which are pure. We would like our programs to be able to interact with the outside world. This means
some abilities must be added to a model of computation in order to allow interaction. The gold
standard for this is [Haskell](https://en.wikipedia.org/wiki/Haskell), with its monadic model of computation. In a good language, effects should be modelled using some kind of language construct, such
as Haskell's monads, but I think the construct will vary for each model of computation.

## Examples of Well-Loved Languages

I will show how the best-designed languages today are simply the minimal additions to already good
models of computation.


| Model of Computation| Language|
|--------------------|----------|
| Untyped Lambda Calculus | Lisp|
| Typed Lambda Calculus | Haskell|
| Predicate Logic | Prolog |
| Rewriting System | Wolfram |
| Actor Model | Smalltalk |
| Interaction Nets | [Kind2](https://github.com/Kindelia/Kind2) |
| Combinatory Logic | APL | 

Hopefully you see that all the languages on the right column are widely admired for being well-designed.
And what unifies them all? They are all strictly based on a model of computation.

Let us discuss the example of Lisp. Lisp is the [minimal wrapper](https://news.ycombinator.com/item?id=29950782) on top of the untyped lambda calculus. It does not include any features
beyound unleashing the inherent power of the lambda calculus. This is the main difference
between Smalltalk and Java. Both are based on the [Actor Model](https://en.wikipedia.org/wiki/Actor_model)
but Smalltalk sticks truthfully to its model of computation, while Java confusedly
borrows concepts from other languages.

## Turing Completeness
Due to Turing Completeness, we can say that all models of computation are equally expressive.
So, it remains to be decided what model we should use. I think we should first choose a model
that is the best for our needs.

## Good Models of Computation
Given all these models of computation, which should we chose as a basis for our languages?
I think it comes down to 2 critera:
- being simple
- having nice properties

For the first point, I think the model should be very simple. I think the [SK Calculus](https://en.wikipedia.org/wiki/SKI_combinator_calculus) is very good in this regard, and it might be the simplest model
of computation that I have ever seen. Turing Machines, although the most well-known example of
a model of computation, are actually very complex and hard to explain. 

For the second point, I mean that the model has properties that make it easy to implement and
fast to run on our given hardware. One model that is very promising is [Interaction Nets](https://en.wikipedia.org/wiki/Interaction_nets#Properties) because they have these properties

- locality (only active pairs can be rewritten)
- linearity (each interaction rule can be applied in constant time)
- strong confluence 

These properties would make an implementation very fast, so I encourage you to try writing
an implementation.


## Advice to Aspiring Language Designers
If you want to design a language, I have some advice for how to do it. The first step is to
choose a model of computation that has not yet been well-explored. For example, I would
not design a language based on lambda calculus because that space has already been perfected
by Lisp and Haskell, and I would not design a langauge based on predicate logic because
Prolog already does a good job there. I would choose a model that has good properties (can
be executed quickly on hardware) and has not been explored by any other language. Right
now I think the field of Linear Logic doesn't have its own industry-strength programming
language. If you think you can design such a language, I would encourage you on.


## Summary
In short, a programming language is nothing but an implentation of a model of computation.

I have come up with a method to design well-loved languages

How to Create an Excellent Programming Lanugage



I just recently got back from attending the [Ross Mathematics Program](https://rossprogram.org/) in Ohio and
I would like to give a review. I came back from the airport giddy with excitement, and I wish that
the Ross Program could go for another week to distract me from school.

## The Math

On the Ross Website, it makes it seem like you will do nothing but math for 6 weeks, and I can say that 
the Ross Program is exactly as advertised. You will get 6 weeks of mathematics. The main curriculum in
number theory was very interesting, and gave me a deeper appreciation of the integers. You may think
that proving that if a is divisible by b, then b < a might be a trivial task, but  at the Ross Program,
we go **FULL RIGOR**, meaning that every proposition must be directly from the axioms with minimal
inference or hand waving (the student's response: "full rigor leads to rigor mortis"). All the problem
sets have interesting problems that test your conceptions of numbers. 

## The Counsellors
All the counsellors at the Ross Program are excited to help you with math and discuss any math topic (Shoutout to Jon!). Just say "I have a math problem" and 10 heads will snap in your direction. Problem sets are
graded daily by the counsellors. Being in a 4-person "family" with a consellor creates a sense
of camaraderie, which is good because I arrived at Ross not knowing anyone.


## Lectures
Special lectures are given by the counsellors and professors from [OSU](https://www.osu.edu/). These are
very exciting and you do not want to miss them. They cover eclectic topics ranging from modular forms
to computation theory. I made the mistake of missing out on Vitaly Berglesson's Pigeonhole lecture series in
the first week and I regret that I did not go. The lectures introduce you to new subjects and really broadened
my conception of what I thought math encompassed. My favourite talk might have been Oscar's talk on the [hyper-reals](https://en.wikipedia.org/wiki/Hyperreal_number)

## The Community
The community was my favorite thing about Ross. It is one thing to solve interesting problems, but it
is quite another to collaborate on problems with people who are just as obsessed with math. 
We all sort of egged each other on to solve more problems and inspired each other. I feel
that the biggest advantage of the Ross Program is that **it prepares you for how life will be in
university**. I.E. in university, you will likely specialize in a subject and hang out with people
in a similar major to discuss your shared passion. 

## The Food
I'd rather not dwell on this subject for too long.


## Tips
If you are going to the Ross Program, I have some tips for you.
- learn how to use a washing machine before you go
- bring some emergency food with you
- **pro tip:** bring a sleeping bag because the dorm beds are unsatisfactory to say the least. If you bring 
a sleeping bag, you will be able to sleep.
- In a similar vein, bring ear-plugs, because there are some people in the next dorm over
who say up very late and you don't want to be kept awake
- The Ross website may claim that you shouldn't bring phones/computers/board games/cards, but 
you will probably be fine if you bring these things.


## Should you go to Ross?
If you would like to do math for 10 hours a day, for 7 days a week, for 6 weeks straight, then apply 
to the Ross Program. I was a bit intimidated at first because I had never done that much math
before, but I really liked the experience. 

Hello, my name is Atticus Kuhn

My Recent Activity