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
A. Background About Aaron Greenspan
1. Defendant Mr. Greenspan is the Chief Executive Officer of Defendant TCC, which operates PlainSite.org, an online repository for legal pleadings from state and federal court lawsuits in the United States.1 Mr. Greenspan is a short seller of Tesla stock and member of the $TSLAQ anti- Tesla group on social media, where Mr. Greenspan goes by the Twitter handle @AaronGreenspan. Mr. Greenspan also posts anti-Tesla messages on social media on behalf of PlainSite.org, using the Twitter handle @PlainSite.
2. Mr. Greenspan has made a career out of threatening and harassing individuals and businesses. His first major target was Facebook. Mr. Greenspan was a Harvard classmate of Mark Zuckerberg’s (“Mr. Zuckerberg”). After Mr. Zuckerberg’s success in founding Facebook, Mr. Greenspan asked Mr. Zuckerberg if Facebook would hire him as Vice President of Engineering. After Mr. Zuckerberg declined, Mr. Greenspan threatened to sue Facebook, claiming that he was Facebook’s true founder. Mr. Greenspan also petitioned the United States Trademark Office to cancel two of Facebook’s registered trademarks for the term “Facebook.” Mr. Greenspan also publicly claimed that Facebook had failed to address various privacy and security issues.2 Mr. Greenspan and Facebook ultimately reached a confidential settlement for a reportedly nominal amount.
3. Mr. Greenspan continued with similar tactics against Random House Publishing and Columbia Pictures. Mr. Greenspan wrote a “memoir” regarding his purported founding of Facebook and asked the Doubleday division of Random House to publish it. Doubleday rejected Mr. Greenspan’s book, and subsequently published a different account of Facebook’s founding by Ben Mezrich titled, The Accidental Billionaires, which later provided the basis for the movie The Social Network. Mr.
Greenspan responded by suing Random House, Mezrich and his company, and Columbia Pictures, which had released The Social Network. Mr. Greenspan asserted a variety of claims, including that Mr. Greenspan had been “defamed by omission” because he was not included as a character in The Accidental Billionaires and The Social Network. Mr. Greenspan’s claims were all dismissed with prejudice by the U.S. District Court for the District of Massachusetts, and the dismissal was unanimously affirmed by the U.S. Court of Appeals for the First Circuit. Greenspan v. Random House, Inc., 895 F. Supp. 2d 206 (D. Mass. 2012), aff’d, 2012 WL 5188792 (1st Cir. Oct. 16, 2012).
4. Undeterred by his failed lawsuit against Random House, Columbia Pictures, and Mezrich, Mr. Greenspan became a serial litigator, filing more than 60 lawsuits (either directly or through organizations he controlled) against over 100 victims. Among them, Mr. Greenspan’s company, TCC, sued California Governor Jerry Brown, then-Attorney General of California Kamala Harris, and various other state government officials, because Greenspan was forced to shut down a startup of his, FaceCash, due to consumer protection law violations. TCC’s suit was dismissed. Think Computer Corp. v. Venchiarutti, No. 5:11-cv-05496-HRL (N.D. Cal. June 25, 2015), ECF No. 70.
5. Additionally, Mr. Greenspan’s company, TCC, sued much of Silicon Valley, including Stanford University, venture capital firms such as Andreesen Horowitz, Kleiner Perkins Caulfield & Byers, and Sequoia Capital, and tech companies such as Coinbase, Facebook (again), Square, and Stripe, among many others, alleging that they operated without money transmitter licenses purportedly required by California law and asserting federal false advertising claims and various state law claims. That suit was dismissed as well. Think Computer Corp. v. Dwolla, Inc., 5-13-CV-02054-EJD, 2014 WL 1266213 (N.D. Cal. Mar. 24, 2014).