184 karma · joined September 3, 2023
1. Tao lacks a fine-tune that accurately follows my instructions. 2. The usage limit on the 100$/month Tao subscription is quite low.
Dismissing results on the basis that Lean code is too long disqualifies this opinion. It is not hard at all to read the Lean result statement, even with very superficial Lean knowledge.
That's like saying that programming is about producing valid programs in various programming languages.
May I present OpenCode, which somehow managed to break copy from terminal: https://github.com/anomalyco/opencode/issues/4283
This is the key point, what is the meaning of "zero knowledge" here? It seems that you need to know something about the implementation, even if it is not the full implementation. Compare this to a zero knowledge proof that you have, say, a factorization gadget, which works by you running the gadget on adversarial input, thus convincing the adversary that you can factor any of their integers. That discloses no implementation details of your factorization gadget, which can be an efficient classical algorithm, a quantum computer, or a phone line to God.
While I believe that Chris Lattner is a great compiler designer, his language design record has been less stellar. Swift bidirectional type inference for instance feels like it was implemented because they had a compiler algorithm that they wanted to use, rather than a genuine need, and is just a completely avoidable problem. Trying to make a HPC language that is also Python compatible was doomed from the start. Hopefully the damage from going into this direction will remain limited.