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

71–80 of 146 posts

Re: Test, don't just verify

#71

Post by AlotOfReading »

nileshtrivedi wrote: post #52

> 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?

You can. Naturals are the default because the kinds of people who write and use proof assistants think usually in terms of natural numbers first rather than the 2-adic numbers mod 2^N we use in programming, or even the plain 2-adics used for algorithmics. It's like mathematicians and 1-based indexing. It violates programming conventions, but the people using it find it easier.

Re: Test, don't just verify

#72

Post by teaearlgraycold »

jesse__ wrote: post #69
Ericson2314 wrote: post #63

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

> 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

Don’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.

Re: Test, don't just verify

#73

Post by Jaxan »

pmontra wrote: post #68
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…

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.

Re: Test, don't just verify

#74

Post by GuB-42 »

"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth

Not that relevant in context as the code in question is used to conclude a formal proof, not the other way around. Buy hey, it is a common quote when talking about proving software and someone has to do it...

Context: https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf

Re: Test, don't just verify

#75

Post by tasuki »

phaedrus wrote: post #36
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 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…

> I wanted to throw a shoe at him.

You should have!

Re: Test, don't just verify

#76

Post by blauditore »

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

Re: Test, don't just verify

#77

Post by hebelehubele »

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.

He's not a native English speaker, for starters. But I like that he didn't fill that gap with an LLM.

Re: Test, don't just verify

#78

Post by tasuki »

lelanthran wrote: post #55
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.

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!

Re: Test, don't just verify

#79

Post by tasuki »

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

Tell me more please: how does one use types in Python? Unfortunately I write Python professionally these days (it is the language that has all the libraries) and hate it with a passion.

Re: Test, don't just verify

#80

Post by imiric »

phaedrus wrote: post #36
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 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…

Agreed.

Besides, it's not like types don't matter in dynamically typed languages. The (competent) programmer still needs to keep types in their head while programming. "Can this function work with a float, or must I pass an int?" "This function expects an iterable, but what happens if I pass a string?" Etc.

I started my career with JavaScript and Python, but over the years I've come to the conclusion that a language that hides types from programmers and does implicit conversion magic in the background does not deliver a better DX. It might make the language more approachable initially, and the idea of faster prototyping might be appealing, but it very quickly leads to maintenance problems and bugs. Before type hinting tools for Python became popular, I worked on many projects where `TypeError` was the #1 exception in Sentry by a large margin.

Gradual and optional typing is better than nothing, but IME if the language doesn't require it, most programmers are lazy and will do the bare minimum to properly add type declarations. Especially with things like TypeScript, which makes many declarations difficult to read, write, and understand.

I think that type inference is a solid middle ground. Types are still statically declared, but the compiler is smart enough to not bother the developer when the type is obvious.

Post reply on HN