A language for verified hard real-time stream processing embedded into Haskell.
An imperative language for safe systems programming embedded into Haskell.
A dependently typed functional programming language where all data is unboxed by default.
Software Foundations in Idris instead of Coq.
A book series on the mathematical foundations of computing, formalized in Coq.
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.