I really like having ~8-12 active Ghostty windows tiled so I can keep an eye on everyone's progress, and then I'll expand one or two for deeper work. Would love to see some sort of auto-expand/contract so I can keep an eye on everything but then when I foreground a pane it grows, or something like that.
>So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task.
Is this true?
e.g. the Riemann hypothesis is in mathlib:
def RiemannHypothesis : Prop :=
∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2
If I construct a term of this type without going via one of the (fairly obvious) soundness holes or a compiler bug, it's very likely proved, no? No matter how inscrutable the proof is from a mathematical perspective. (Translating it into something mathematicians understand is a separate question, but that's not really what I'm asking.)
Non-async functions are absolutely blocking. The question is if they’re expected to block for a meaningful amount of time, which is generally suggested by your async runtime.
It’s really not that bad, you might just need a better mental model of what’s actually happening.
You can absolutely do global knowledge in proc macros via the filesystem and commit their output to version control: https://github.com/trevyn/turbosql
You can introduce side effects to a proc macro (but please avoid if at all possible), but you cannot control the order in which proc macros are run. If you need to reason about the global schema while generating code, that won’t work.