Benki → Bookmarks

His preferred tax system: a personal expenditures tax. It works like the following:

• Idea: Tax only consumption, but in a progressive way.
• How? Tax people’s income (similar to how it is done today, but regardless of the source of income), deducting what they leave in savings (be it checking accounts, stocks, whatever).

What’s nice about this is that it is income-agnostic (capital gains and wages are taxed the same) and progressive while still incentivizing people to save.

Plus a Georgist land value tax, of course.

How to encode inductive data types in Kind’s type system.

A small functional programming and proof language with accessible syntax.

Comparison of effect systems for Haskell.

Runtime for functional programs. Claims to be very efficient. Lazy, garbage-collection-free, parallel, and beta-optimal.

Comparison between different monadic effect systems.

I am still hoping Scala 3 gets a built-in effect system eventually so that all of this can go away. Monadic style does not fit the language well.

A language for the description of cryptographic algorithms.

Examples:

• SipHash
• Keccak

Functional programming language for the JVM with row types, algebraic effects, and embedded Datalog.

JVM back end for Idris 2.

A one-binary initramfs.

A framework for secure booting, building on top of whatever secure booting functionality the firmware provides and then taking over from there.

Using Linux as firmware and as a boot loader.

We need to be flexible and build our systems in such a way that we can switch out cryptographic algorithms as new attacks come along.

What worked in the past does not necessarily work today. Evolving defensive measures and notions of what “unthinkable” actions are force changes in strategy.

Converts a pattern description in English into a regular expression with the help of artificial intelligence.

A dependently-typed programming language and interactive theorem prover with an extrinsic type system based on the untyped lambda calculus.

Air conditioning works, but is not sustainable. The paper discusses alternatives.

Under most circumstances, anyway.

Chris Auld’s critique of Steve Keen.