← Feed

Posts

• View post

  After a long discussion on the Lean Zulip, Mario Carneiro has shown that the Calculus of Inductive Constructions (in its full version w/ large elimination of Acc) + Excluded Middle proves that ZF is consistent: https://arxiv.org/abs/2609.23143 It is fairly simple to show that Aczel’s type of sets as well-founded trees is a model of ZF without Replacement, and even a bit further, that the iterative hierarchy V_alpha exists for all ordinals alpha, but Replacement seems very analogous to Unique Cho...

• View post

  After playing around with various attempts to construct models of ZF (or IZF) in the Calculus of Inductive Constructions, I can say that CiC (even with LEM) is severely deficient compared to ZF/IZF in terms of what can be done without assuming some form of Choice. I think that Lean's banishment of these problems by just assuming Choice throughout the ecosystem might be no small part of its appeal to mathematicians.

• View post

  I don't even eat dumplings anymore, I just buy into a dumpling REIT

• View post

  @joe@f.duriansoftware.com Zeroing is adding a new "row" syntax, motivated by token efficiency: type Point x 132 y 132 fn sum i32 point Point ret + point.x point.y pub fn main Void world World ! let point Point . x 40 y 2 let total sum point if == total 42 check world.out.write "ok\n"

• View post

  I’ve seen a number of people speak about a representation of datatypes in ML where a datatype is given by a module with an abstract type and its constructors. Obviously, this is missing some additional information to define pattern matching, e.g. a recursor. Has anyone actually worked out all of the details?

• View post

• View post

  The latest Lean soundness hole (https://github.com/leanprover/lean4/issues/14576), which also affects alternative implementations of the kernel, is proof that God only ever intended for us to use W-types, and certainly not nested inductives.

• View post

  we need to consider deceleration

• View post

  @joe@f.duriansoftware.com @slava@mathstodon.xyz I know we talked about this as part of a shitpost thread, but can either of you think of a good way to combine traits (i.e. type classes) and bytewise equality / hashing while still preserving as much parametricity as possible? The natural thing is to have some marker trait with C++ style specialization, but that destroys a lot of the properties that you would want. @joe@f.duriansoftware.com mentioned (jokingly but maybe not) to just make it requi...

• View post

  @dotstdy@mastodon.social @ianh@mastodon.social Has any recent language adopted uncurried single arg style where product types are used for multiple args rather than implicit currying? I know that Swift originally started in this direction, but I forget the actual reason why they backed away from this. Can you refresh my memory, @joe@f.duriansoftware.com ?

• View post

  @joe@f.duriansoftware.com Why did Swift never get block expressions? Was nice trailing lambda syntax worth more?

• View post

  I'm always curious about peoples' pure C compiler codebases, so I took a look at Vercel's new Zero language (https://zerolang.ai). You can tell that someone is just fed up with the bullshit of using unions in C when you see this: struct Expr { ExprKind kind; char *text; char *resolved_type; bool moves_ownership; bool mutable_borrow; bool bool_value; bool array_repeat; Expr *left; Expr *right; ExprVec args; TypeArgVec type_args; TypeArgVec checked_type_args;...

• View post

  A conversation with @jiribenes about parsers in Effekt (https://effekt-lang.org) made me realize this interesting question: can determinization of non-deterministic LL(1) parsers a specific of a general program transformation for programs with a nondeterminism effect?

• View post

  I treat garbage collected languages like Undertale and always go for a pacifist run.

• View post

  @joe It occurred to me while walking today that if all of the arguments for stackless coroutines are valid, then Rust should actually switch to CPS for compiling all (non-recursive?) functions.

• View post

  C++ is the final stage of programming languages, a pure Simulacrum with no relationship to reality whatsoever.

• View post

  @jonmsterling Do you think it is possible to make an ML/prover combo in the LCF style so that the metalanguage’s module/locale/… system can adequately model mathematical hierarchies, or is the pure LCF architecture relegated to history?

• View post

  @joe@f.duriansoftware.com What do you think is the maximal subset of effect handlers that can be supported well in a C-like language (with a C-like compilation model)?

• View post

  GitHub is the only web app that got less reliable after it stopped being (as much of) a Rails monolith.

• View post

  For a long time I believed that one of the advantages of dependent type theory for applications to SW/HW verification was that it naturally incorporates proof by reflection (since the kernel type checker can do nontrivial computations). In particular, this comes in handy when dealing with decision procedures. Even when they can produce a proof (e.g. SAT solvers producing resolution proofs), the proof term is usually too large for this approach to scale to real problems. And there are many cases...

• View post

  LLVM is so afraid of optimizing around atomics that it is more pessimistic about an inlined atomic than an extern function: https://discourse.llvm.org/t/missed-store-forwarding-in-the-presence-of-atomic-operations/90653

• View post

  Rust's lack of relative enum constructor names makes me dread having two enums with the same name.

• View post

  The province of Saskatchewan (except for the Alberta border city of Lloydminster) has never followed daylight savings time, opting for permanent Central Standard Time. Alberta is now adopting permanent Mountain Daylight Time, which is synchronized with Saskatchewan. This is a great real-world example of the difference between intensional and extensional equality.

• View post

  Despite Rust deliberately making your life miserable if you dare attempt to use unstable features that have existed for years, I caved and used the `gen_blocks` feature (https://github.com/rust-lang/rfcs/pull/3513) to reimplement a complicated iterator whose logic I had initially written by hand. They should really finish sanding the edges and stabilize this feature so that nobody needs to write iterators as explicit state machines ever again.

• View post

  You either die a hero or live long enough to break subject reduction.

• View post

  One of the most pressing naming discussions of our time: when you have a sum type `Token`, `Expr`, etc. and then a wrapper containing it + some common info (like trivia for `Token`, a source span for other nodes) what do you call the two? I used to always default to `Expr` and `ExprData`, but rustc generally defaults to `ExprKind` and `Expr`, despite `ExprKind` containing lots of data beyond just the plain `enum` that it represents: https://doc.rust-lang.org/beta/nightly-rustc/rustc_ast/ast/enum...

• View post

  I just saw an ad that began with “inflight Wi-Fi has come a long way since I was a kid”. I am officially unc, also chopped.

• View post

  combined Davos/POPL keynote ideas "You'll own nothing and you'll be happy: a garbage collection rejoinder" "The great shift/reset: a continuation or delimiter of progress?" "Late-staged programming: are the economics of macros sustainable?"

• View post

  Can someone please tell Leo that these obviously LLM-generated blog posts are cringe? https://leodemoura.github.io/blog/2026-4-2-why-lean/

• View post

  Sci-fi novel idea: you're a human who wakes up with amnesia every day and reads your AGENTS.md file.