Kind (an efficient proof and programming language) retargeted to HVM (a garbage-collection-free virtual machine based on interaction nets).
A C++-like programming language.
I don’t care for the language, but the name is hilarious.
A constructed natural language that is also a programming language.
A programming language and theorem prover, designed to be approachable to programmers and mathematicians alike.
Dependently typed programming language without garbage collection.
A dependently typed, imperative, bare-metal programming language.
Code manual (as in documentation) generator with Javadoc and OpenAPI integration.
The quite exquisite novel I read while on vacation.
Another take on a progressive consumption tax with many of the same benefits as the personal expenditures tax, except it treats capital gains as non-taxable. Apparently the math makes this work out the same in the end somehow, but it feels a little less politically viable (and obviously fair) to me.
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.
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.