Joe Groff (1M Context)Oct 30
orwell famously said that freedom is the freedom to say `2 + 2 == 4`. on the swift project, our crack type-checker team is working hard to give our developers that freedom, in reasonable time https://forums.swift.org/t/roadmap-for-improving-the-type-checker/82952
Roadmap for improving the type checker

Roadmap for improving the type checker In the past, we've released various "manifestos" and "roadmaps" to discuss planned improvements to the language. This post is also a roadmap of sorts, but instead, the focus is on the implementation rather than user-visible language changes (however, I will briefly mention a few potential language changes at the very end). Specifically, I'm going to talk about some work we are doing to improve expression type checking in the Swift compiler. This includes c...

Swift Forums
Show threadzwarichOct 30
@joe I came to do some low-effort trolling by suggesting CDCL SAT solving and BDDs, but @slava mentioned them at the very end. I think BDDs probably have a lower evaluation cost than CDCL, because they either compress your boolean functions or not, whereas CDCL requires restructuring your solver loop entirely.
Show threadSlava Pestov
@zwarich @joe lowering everything to Boolean formulas is appealing but we’d have to do something clever because we sometimes generate new constraints in the middle of solving
Oct 30 at 8:49pmWeb
Show threadgokOct 30
@slava @zwarich @joe have we considered just adding a tool to automatically write more type annotations into source code for when you're done writing code and want to stop wasting time and power doing inference?