Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Test, don't just verify

alperenkeles.com

Post reply on HN
Print view View original

141–146 of 146 posts

Re: Test, don't just verify

#141

Post by anon-3988 »

Ericson2314 wrote: post #65
anon-3988 wrote: post #28

Before we start writing Lean. Perhaps we can start with something "dumber" like Rust or any typed program. If you want to write something correct, or you care about correctness, you should not be using dynamic languages. The most useful and used type of test is type checking. Type errors, especially once you have designed your types to be correct by construction, is extremely, extremely useful for LLMs. Once you have…

> To me, panic is the most laziest and worst ways to put in a specification. This why the "existing programs don't have specs!" Hand-ringing is entirely premature. Just about every code base today has error modes the authors think won't happen. All you have to do is start proving they won't happen. And if you do this, you will begin a long journey that ends up with a formal spec for, at least, a good part of your pro…

Orrrr just use an API that returns Option, then bubble it up or manually panic if that's what you want?

Re: Test, don't just verify

#142

Post by anon-3988 »

pron wrote: post #101
anon-3988 wrote: post #28

Before we start writing Lean. Perhaps we can start with something "dumber" like Rust or any typed program. If you want to write something correct, or you care about correctness, you should not be using dynamic languages. The most useful and used type of test is type checking. Type errors, especially once you have designed your types to be correct by construction, is extremely, extremely useful for LLMs. Once you have…

> Perhaps we can start with something "dumber" like Rust or any typed program. If you want to write something correct, or you care about correctness, you should not be using dynamic languages. The most useful and used type of test is type checking. Lean or TLA+ are to Rust/Java/Haskell's type systems what algebraic topology and non-linear PDEs are to "one potato, two potatoes". The level of "correctness" achievable w…

I mean..sure, but I just want the first 80%. We don't have that. Instead, we are building kernels and infrastructure using bash scripts that who knows does what. We need a tool that is solid and rigid that LLMs can use to go through all of that.

It should be something that is familiar (so imperative style like C), easier to read (perhaps with type inference) and have strong modern type system (just give me sum type is enough for gods sake). Perhaps Python with (real) types.

Re: Test, don't just verify

#143

Post by Ericson2314 »

jesse__ wrote: post #125
Ericson2314 wrote: post #115

Earlier quoted context omitted.

I'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.

> great languages like [...] Haskell We have very different opinions on what makes a great language

Then I'm surprised you agreed with any of what I wrote!

Re: Test, don't just verify

#144

Post by pron »

anon-3988 wrote: post #142
pron wrote: post #101

Earlier quoted context omitted.

> Perhaps we can start with something "dumber" like Rust or any typed program. If you want to write something correct, or you care about correctness, you should not be using dynamic languages. The most useful and used type of test is type checking. Lean or TLA+ are to Rust/Java/Haskell's type systems what algebraic topology and non-linear PDEs are to "one potato, two potatoes". The level of "correctness" achievable w…

I mean..sure, but I just want the first 80%. We don't have that. Instead, we are building kernels and infrastructure using bash scripts that who knows does what. We need a tool that is solid and rigid that LLMs can use to go through all of that. It should be something that is familiar (so imperative style like C), easier to read (perhaps with type inference) and have strong modern type system (just give me sum type i…

But if LLMs get to the point they're smart enough to deal with the tricker aspects of programming, what makes you think they need help with the easier parts? Conversely, if they're not smart enough to deal with the trickier parts, why would a little help move the needle much? Despite trying, research has not been able to find a significant general[1] effect of language design on correctness or productivity for human programmers (at least among more-or-less high level languages; I'm not talking Java vs Assembly). We all have our preferences, and we tend to think they're universal, but it's precisely because of this bias that empirical study is needed, and it's not been conclusive.

If there's no big impact on humans, why assume there would be one for LLMs? I'm not saying that LLMs think like humans, but the default hypothesis should be that something doesn't make a big difference if there's no example in which it does. In other words, if something does not have a known effect, we shouldn't assume that it will in this case (I mean, it could, but we'll need to first find good empirical evidence for that).

[1]: Research did find some differences between TypeScript and JavaScript specifically, but that result hasn't generalised.

Re: Test, don't just verify

#145

Post by jesse__ »

Ericson2314 wrote: post #143
jesse__ wrote: post #125

Earlier quoted context omitted.

> great languages like [...] Haskell We have very different opinions on what makes a great language

Then I'm surprised you agreed with any of what I wrote!

I 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-reas...

Post reply on HN