Slacker News Slacker News logo featuring a lazy sloth with a folded newspaper hat
  • top
  • new
  • show
  • ask
  • jobs
Library
← Back to context

Comment by dlahoda

4 days ago

One can just use Lean4 and panic each time it asks proof. 5 of 5. Community is PhDs and geniuses. Types are values, full uniformity = simplicity. Perf > Swift because reference counters eliminated at compile time. AI likes types. Just panic when Lean4 asks for proofs. Backed by biggest corps out there. Macro are best of Rust and Scala.

0 comments

dlahoda

Reply

No comments yet

Contribute on Hacker News ↗

Slacker News

Product

  • API Reference
  • Hacker News RSS
  • Source on GitHub

Community

  • Support Ukraine
  • Equal Justice Initiative
  • GiveWell Charities