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

51–60 of 146 posts

Re: Test, don't just verify

#51

Post by baq »

seg_lol wrote: post #44
phaedrus wrote: post #36

Earlier quoted context omitted.

I once attended a talk by someone who is or was big in the node.js world. He opened with the premise, "a static type check is just a stand-in for a unit test." I wanted to throw a shoe at him. A static type check doesn't stand in for "a" unit test; static typing stands in for an unbounded number of unit tests. Put another way, this common misconception by users of languages like Javascript and Python that unit testin…

Hundreds of unit tests replace a type. Start using properties and it is in the thousands. Most code should be typed. Python is great for prototypes, but once the prototype gels, you need types.

Good that Python supports types then

Re: Test, don't just verify

#52

Post by nileshtrivedi »

> proof assistants, traditionally, don't use our classic two's complement integers packed into words in our memory, they use Peano numbers

Why can't we just prove theorems about the standard two's complement integers, instead of Nat?

Re: Test, don't just verify

#53

Post by gaogao »

xp84 wrote: post #45

For the verification experts: (and forgive me because I have almost zero of the math understanding of this stuff) > This makes formal verification a prime target for AI-assisted programming. Given that we have a formal specification, we can just let the machine wander around for hours, days, even weeks. Is this sentiment completely discounting that there can be many possible ways to write program that satisfies certa…

Yup, I've already spent like $20k using Claude to verify things, so like there's probably some room for cost cutting.

Re: Test, don't just verify

#54

Post by didip »

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…

I agree. And learning a typed language is significantly easier now that AI can explain everything. The types also help AI to write a correct code. A very positive feedback loop.

Re: Test, don't just verify

#55

Post by lelanthran »

seg_lol wrote: post #44
phaedrus wrote: post #36

Earlier quoted context omitted.

I once attended a talk by someone who is or was big in the node.js world. He opened with the premise, "a static type check is just a stand-in for a unit test." I wanted to throw a shoe at him. A static type check doesn't stand in for "a" unit test; static typing stands in for an unbounded number of unit tests. Put another way, this common misconception by users of languages like Javascript and Python that unit testin…

Hundreds of unit tests replace a type. Start using properties and it is in the thousands. Most code should be typed. Python is great for prototypes, but once the prototype gels, you need types.

I've always hated Python. Could never enjoy it at all. Pretty much the same poor DX as PHP, Javascript, Ruby, etc.

Finally set up neovim with pyright; use types on every single fucking thing, and now I love Python[1].

Can't wait to see TC39 become a reality (learned about it just this past week on HN, actually). Maybe I'll enjoy Javascript too.

--------------------

[1] Within reason; the packaging experience is still extremely poor!

Re: Test, don't just verify

#56

Post by lelanthran »

baq wrote: post #51
seg_lol wrote: post #44

Earlier quoted context omitted.

Hundreds of unit tests replace a type. Start using properties and it is in the thousands. Most code should be typed. Python is great for prototypes, but once the prototype gels, you need types.

Good that Python supports types then

> Good that Python supports types then

"Optional typing" is not the same as "Static typing".

Great, my program will crash, because I forgot to opt-in to typing :-/

Re: Test, don't just verify

#57

Post by SR2Z »

baq wrote: post #51
seg_lol wrote: post #44

Earlier quoted context omitted.

Hundreds of unit tests replace a type. Start using properties and it is in the thousands. Most code should be typed. Python is great for prototypes, but once the prototype gels, you need types.

Good that Python supports types then

Poorly, though, and with lots of edge cases and foot guns to make you miserable once your code calls out to numpy or gets some JSON.

Re: Test, don't just verify

#58

Post by enceladus76 »

MetaWhirledPeas wrote: post #34

I lack the level of education and eloquence of the author, but I have my own notion that I think agrees with them: Specification is difficult and slow, and bugs do not care whether they are part of the official specification or not. Some software needs formal verification, but all software needs testing. On another subject... > Tests are great at finding bugs ... but they cannot prove the absence of bugs. I wish more…

Unless people therefore decide that testing unnecessary... Which has happened a lot in academia. One of the reasons testing is not being taught that well on some universities...

Re: Test, don't just verify

#59

Post by lelanthran »

marcosdumay wrote: post #11
getregistered wrote: post #3

> AI-assisted programming pushes the limits of programming from what you can implement to what you can specify and what you can verify. This really resonates. We can write code a lot faster than we can safely deploy it at the moment.

> 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 code to test.

Re: Test, don't just verify

#60

Post by aidenn0 »

See also Regehr's example[1] where a formally verified C compiler generates incorrect output because of an inconsistent value in (TL;DR: The compiler can pick whether "char" is signed or unsigned. Compcert picked one, but the linux system header used the other for CHAR_MIN and CHAR_MAX).

1: https://blog.regehr.org/archives/482 there were many issues here, not just with compcert

Post reply on HN