4 ms·
This blog post is out of its depth - Lean will optimize peano arithmetic with binary bignums underneath the hood - Property based checking and proof search al
by Ericson2314 10mo ago
This blog post is out of its depth
- Lean will optimize peano arithmetic with binary bignums underneath the hood
- Property based checking and proof search already exist on a continuum, because counterexamples are a valid (dis)proof technique. This should surprise no writer of tactics.
- the lack of formal specs for existing software should become less a problem for greenfield software after these techniques go mainstream. People will be incentivized to actually figure out what they want, and successfully doing so vastly improves project management.
Finally, and most importantly, people thinking that there is a "big specification" and then "big implementation" are totally missing the mark. Remember tools like lean are just More Types. When we program with types, do we have a single big type and a single untyped term, paired together? Absolutely not.
As always, the key to productive software development is more and more libraries. Fancier types will allow writing more interesting libraries that tackle the "reusable core" of many tasks.
For example, do you want to write a "polymorphic web app" that can be instantiated with a arbitrary SQL Schema? Ideas like that become describable.
- jesse__ 10mo ago> the key to productive software development is more and more libraries You had me until this statement. The idea that "more and more libraries" is going to solve the (rather large) quality problems we have in the software industry is .. misguided. see: https://www.folklore.org/Negative_2000_Lines_Of_Code.html https://www.folklore.org/Negative_2000_Lines_Of_Code.html https://caseymuratori.com/blog_0031 https://caseymuratori.com/blog_0031
- teaearlgraycold 10mo agoDon’t use a library unless you really need it. Someone recently recommended I add Zod to a project where I am only validating two different JSON objects in the entire project. I like Zod, but I already wrote the functions to progressively prove out the type in vanilla JS. Less is more, including other people’s libraries.
- jesse__ 10mo agoAgreed.
- swid 10mo agoGo Proverb: A little copying is better than a big dependency.
- teaearlgraycold 10mo ago100% agree. This actually makes AI-aided development a big improvement (as long as you’re careful). You can have an LLM write you a little function, or extract the correct one from a big library, and inline it into your module.
- Ericson2314 10mo agoI'm talking great libraries in great languages. Like how the kmettverse revolutionized writing Haskell. Libraries that make you completely reconsider what it is you're trying to do. Most people use shit libraries in shit languages. NPM slopfests have no bearing on what I'm talking about.
- jesse__ 10mo ago> great languages like [...] Haskell We have very different opinions on what makes a great language
- Ericson2314 10mo agoThen I'm surprised you agreed with any of what I wrote!
- jesse__ 10mo agoI mean, I agree with the notion that a great type system is part of a great language, but the type system is only a small part of the overall whole. Haskell has a great type system, but it fails miserably at many trivial tasks I care about : 1) sum 1 million integers == stackoverflow (big lul) 2) massive memory cliffs for using the wrong type [1], which is not uncommon 3) poor metaprogramming facilities 4) difficult documentation [1] https://stackoverflow.com/questions/76470000/is-there-a-reason-my-haskell-program-uses-so-much-memory https://stackoverflow.com/questions/76470000/is-there-a-reas...
- dalmo3 10mo ago> People will be incentivized to actually figure out what they want That's the AGI I want to see.