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

121–130 of 146 posts

Re: Test, don't just verify

#121

Post by array_key_first »

lelanthran wrote: post #89
paulddraper wrote: post #83

Earlier quoted context omitted.

C has void pointers.

> C has void pointers. And? Void pointers are not the default type :-/ With Python I have to do extra work to get type errors. With C I have to do extra work to hide the type errors. I am battling to understand the point you are making.

He's probably conflating static and strong typing.

C is statically typed, but weakly typed - you need to throw away types to do a bunch of run of the mill things. Python is dynamically typed, but strongly typed, where it will just fail if typed don't resolve.

C# and C++ are both statically typed and strongly typed, although C# more than C++ in practice.

Re: Test, don't just verify

#122

Post by smohare »

zahlman wrote: post #100
tasuki wrote: post #78

Earlier quoted context omitted.

I've never seen types used correctly in Python. A `tuple` is not even a type! It's a type constructor!

The distinction you are trying to make is nonsensical in Python's object model. Types are inherently callable, and calling them constructs (i.e. instantiates) the type (normally; this can be overridden, by design). There is also no type->kind->category hierarchy; `type` itself is an object, which is its own type. When you're at a level of theory where terms like "type constructor" are natural, it's unreasonable to ex…

[dead]

Re: Test, don't just verify

#123

Post by baq »

tasuki wrote: post #78
lelanthran wrote: post #55

Earlier quoted context omitted.

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 sti…

I've never seen types used correctly in Python. A `tuple` is not even a type! It's a type constructor!

I’ve been doing Python and Typescript professionally, Python for almost two decades, Typescript for last 5 years and I can very confidently say that it doesn’t matter.

Besides, you see to be confusing Python run-time with Python typecheck-time, theoretically unfortunate, but again practically irrelevant distinction. (Unfortunate since Python typecheck is basically a different language than Python execution; irrelevant, because the right subsets of both align well.)

Re: Test, don't just verify

#125

Post by jesse__ »

Ericson2314 wrote: post #115
jesse__ wrote: post #69

Earlier quoted context omitted.

> 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://caseymuratori.com/blog_0031

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

Re: Test, don't just verify

#126

Post by pron »

pron wrote: post #97

I find this discourse about AI and formal verification of software very confusing. It's like someone saying, let's assume I can somehow get a crane that would lift that vintage car and place it in my 15th floor apartment living room, but what will I do with my suitcases? All the problems mentioned in the article are serious. They're also easier than the problem of getting an AI to automatically prove at least hundred…

What I'm trying to say is that a machine that can reliably write a complex, large piece of software and prove its correctness - somethng that, BTW, humans are not currently capable of doing - is also likely a machine that can do that from the prompt: Write a piece of software that will be popular among women aged 35-65, let alone "write a spreadsheet that's as powerful as excel but easier to use". Of course, once that happens, the market value of any such software will drop to zero, because anyone could give such a prompt. In fact, there would be no need for software as we know it because the AI could just do what the software is supposed to do (although perhaps it would choose to create an executable as an implementation detail).

What I see is people spending a lot of time imagining how we would work with an AI that could solve some huge problems and at the same time fail to solve easier problems. I don't understand the point of the exercise.

Re: Test, don't just verify

#127

Post by Jensson »

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…

> Right now, a single developer with Claude code can very easily overwhelm even a couple of testers with new code to test.

Because there are endless errors and problems that never gets fixed with AI coding. The reason testers ran out of things to test before was that developers tested themselves before sending it over, if you take a bunch of cowboy coders coding thousands of lines a day with no testing whatsoever before throwing it over to the testers you would say you don't have enough testers even if you had thousands.

Re: Test, don't just verify

#128

Post by zahlman »

array_key_first wrote: post #120
zahlman wrote: post #95

Earlier quoted context omitted.

> it is simply more enjoyable to design the types in your program than to write unit tests. I have tried both and I have no idea what you're talking about. > Making yourself think about “for all x” rather than a concrete x forces your brain to consider deeply the properties of x being used. The entire point of dynamic typing is that you can think about interfaces rather than concrete types, which entails deep conside…

That's not the entire point of dynamic typing, because all the interface stuff comes from statically typed languages. Some* dynamic languages borrowed it, but most use "implicit" interfaces - where the interface is whatever kind of works, I guess.

> because all the interface stuff comes from statically typed languages.

No, it doesn't. It comes from theory that came after the languages.

> Some* dynamic languages borrowed it, but most use "implicit" interfaces

An implicit interface is an interface, and is exactly the sort of thing I'm talking about in GP. The point is that you think about the object in terms of its capabilities, rather than some proven-up-front categorization that it fits into. What it does, not what it is.

Re: Test, don't just verify

#129

Post by senderista »

I think the article still sells formal specification a bit short in a few areas:

- A formal spec can be used to derive randomly generated tests attempting to find counterexamples to spec invariants (which the article hinted at but didn't describe explicitly)

- A formal spec can be used as input to a model checker, which will try to find counterexamples to spec invariants via bounded exploration of the model's state space

- A formal spec can be used to find spec invariant violations by analyzing traces from production systems

What all these examples have in common is that they attempt to falsify, not verify, that the spec accurately describes the desired design properties or the actual implementation. That tends to be much more feasible than an actual proof.

Re: Test, don't just verify

#130

Post by senderista »

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…

There's a pretty fundamental difference: TDD is about avoiding up-front design, while formal specification literally is up-front design.
Post reply on HN