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

101–110 of 146 posts

Re: Test, don't just verify

#101

Post by pron »

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 with such simple type systems is so negligible in comparison to the things you can express and prove in rich formal mathematics languages that they barely leave an impression (they do make some grunt work easier, but if we're talking about a world where a machine can do the more complicated things, a little more grunt work doesn't matter).

Re: Test, don't just verify

#102

Post by zahlman »

Jaxan wrote: post #73
pmontra wrote: post #68

Earlier quoted context omitted.

Good luck using static typing to model many real world unit tests for the programming languages people use most. I start with an easy example: those records should be sorted by date of birth. We can move on to more complicated scenarios.

The comment didn’t claim that types are a stand in for tests either! IMO, they are orthogonal.

The comment explicitly set out to refute the idea "...that unit testing is just as good as type checking" by describing the former as simply inferior.

Re: Test, don't just verify

#103

Post by zahlman »

chamomeal wrote: post #86
brabel wrote: post #37

Earlier quoted context omitted.

Common Lisp as well. I can’t explain why, but type errors are just not something I struggle with in Common Lisp! But it is in JS and Python for sure. Maybe someone knows why it feels different?

I think it’s cause there’s less imperative code and side effects to track data transformations through. Like any random JS/php app is probably a huge pile of loops and if statements. To track what happens to the data, you need to run the whole program in your head. “And now it adds that property to the object in the outer scope, and now that object gets sorted, now it hits the database… ok…”. Whereas in clojure most…

> Like any random JS/php app is probably a huge pile of loops and if statements. To track what happens to the data, you need to run the whole program in your head. “And now it adds that property to the object in the outer scope, and now that object gets sorted, now it hits the database… ok…”. Whereas in clojure most functions are either a single atomic transformation to a set of data, or batch of side effects. You still have to run it through your head, but you can do it more piece-by-piece instead of having to understand a 1,000 method with class states being auto loaded and mutated all over the place. Also you have a REPL to try stuff out as you go.

Nothing really forces you to write imperative code in a large fraction of cases, and typically the state-change operations can be quite localized within the code. And of course JavaScript and Python both also have REPLs.

Re: Test, don't just verify

#104

Post by zahlman »

blauditore wrote: post #76
MarkMarine wrote: post #61

This is an aside because I agree with the author’s core point, but spelling, grammatical errors, and typos actually imply something authored by a human now. This sentence: “It affects point number 1 because AI-assisted programming is a very natural fit fot specification-driven development.” made me smile. Reading something hand made that hadn’t been through the filters and presses of modern internet writing.

To my surprise, I recently found a typo in AI-generated code. It's rare though

There are typos all over the training data, and people offering RLHF feedback can overlook them.

Re: Test, don't just verify

#105

Post by zahlman »

altmanaltman wrote: post #84
layer8 wrote: post #46

Earlier quoted context omitted.

With double-entry bookkeeping, the only way an error can slip through is if you make the same error on both sides, or else they wouldn’t be balanced. A similar thing is true for testing: If you make both an error in your test and in your implementation, they can cancel out and appear to be error-free. I don’t quite agree with that reasoning, however, because a test that fails to test the property it should test for i…

> With double-entry bookkeeping, the only way an error can slip through is if you make the same error on both sides, or else they wouldn’t be balanced. A similar thing is true for testing: If you make both an error in your test and in your implementation, they can cancel out and appear to be error-free. Yeah but it's very different from tests vrs code though, right? Every entry has two sides at least and you do it to…

> Yeah but it's very different from tests vrs code though, right? Every entry has two sides at least and you do it together, they are not independent like test and code.

The point of the current thread is that the use of AI coding agents threatens to disrupt that. For example, they could observe a true positive test failure and opt to modify the test to ensure a pass instead.

Re: Test, don't just verify

#106

Post by marcosdumay »

lelanthran wrote: post #59
marcosdumay wrote: post #11

Earlier quoted context omitted.

> We can write code a lot faster than we can safely deploy it at the moment. We always could. That has been true since the days we programmed computers by plugging jumper wires into a panel.

> We always could. That has been true since the days we programmed computers by plugging jumper wires into a panel. That's news to me, and I'm an ancient greybeard in development. If you have a team of 1x f/time developer and 1x f/time tester, the tester would be spending about half their day doing nothing. Right now , a single developer with Claude code can very easily overwhelm even a couple of testers with new cod…

> the tester would be spending about half their day doing nothing

That's because the developer would be spending 2/3 of their day fixing the problems the tester already found.

And the time spent writing new code has always been a rounding error from 0.

Re: Test, don't just verify

#107

Post by Veserv »

zahlman wrote: post #102
Jaxan wrote: post #73

Earlier quoted context omitted.

The comment didn’t claim that types are a stand in for tests either! IMO, they are orthogonal.

The comment explicitly set out to refute the idea "...that unit testing is just as good as type checking" by describing the former as simply inferior.

No. They refuted the claim that "a static type check is just a stand-in for a unit test". That is a claim that you can just remove your type checks and replace them with unit tests at no loss. The comment stated that removing a type check just so you can replace it with a unit test is inferior. The prior state was already pre-supposed to have a type check/type checkable condition that you could replace.

That is the literal converse of the claim in the response to that comment arguing that the comment stated that all unit tests can be replaced with type checks. Those are not at all the same claim.

To make it even more clear the comment said: I saw a talk that said Type Check -> Unit Test. I said that is silly.

Response said: Unit Test -> Type Check is not reasonable. So clearly your claim that Type Check -> Unit Test is silly is wrong.

Re: Test, don't just verify

#108

Post by i_am_a_peasant »

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…

a rust to js transpiler would be pretty sweet. idk if someone has turned rust into a frontend language yet like typescript.

Re: Test, don't just verify

#109

Post by antupis »

andrewmutz wrote: post #17

I agree completely with the author that AI assisted coding pushes the bottleneck to verification of the code. But you don't really need complete formal verification to get these benefits. TDD gets you a lot of them as well. Perhaps your verification is less certain, but it's much easier to get high automated test coverage than it is to get a formally verifiable codebase. I think AI assisted coding is going to cause a…

Mainstream has been slowly adapting xp like last 20 years, devops first and now pair programming with agents and tdd.

Re: Test, don't just verify

#110

Post by NlightNFotis »

ozim wrote: post #92

I smell vaporware. Formal verification is easy on easy stuff like simple functions - complex functions it might be impossible. Then you most likely will get bunch of snake oil salesmen promising that you can verify full system…

What is a complex function to you, and why do you think it’s impossible to verify properties of them?
Post reply on HN