Static verification of function pre- and post-conditions for Rust.
Not as powerful as full dependent types, but could be a good middle ground between something like ATS and down-to-earth plain Rust.
A Java library for defining JMeter performance tests.
An imperative programming language for verified bare-metal programming. Currently targets RISC-V only.
A dependently typed domain-specific language for hardware design, embedded into Agda.
A low-level, dependently typed, impure functional programming language.
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.