Live data from Hacker News

Test, don't just verify

alperenkeles.com

91–100 of 146 posts

Re: Test, don't just verify

#91

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…

> People will be incentivized to actually figure out what they want

That's the AGI I want to see.

Re: Test, don't just verify

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

Re: Test, don't just verify

#93
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…

> Statically typed clojure

Well, if you also like Common Lisp, there's Coalton, which is Common Lisp with a Haskell-like type system: https://coalton-lang.github.io/

Re: Test, don't just verify

#94
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…

Didn't get the bit about TC39 - it is just a group. It has nothing to do with types in JS.

Re: Test, don't just verify

#95
post #38

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…

Plus, it is simply more enjoyable to design the types in your program than to write unit tests. The fun factor comes from operating on a higher level of abstraction and engages more of your brain’s puzzle-solving mode than just writing unit tests. Making yourself think about “for all x” rather than a concrete x forces your brain to consider deeply the properties of x being used.

> 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 consideration of the properties of the object (semantics of the provided interface).

Re: Test, don't just verify

#96
post #94

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…

Didn't get the bit about TC39 - it is just a group. It has nothing to do with types in JS.

Sorry, I should have been clearer about which proposal I was talking about:

https://github.com/tc39/proposal-type-annotations

Re: Test, don't just verify

#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 hundreds of correctness properties on programs that are hundreds of thousand, if not millions of lines long. Bringing higher mathematics into the discussion is also unhelpful. Proofs of interesting mathematical theorems require ingenuity and creativity that isn't needed in proving software correct, but they also require orders of magnitude fewer lemmas and inference steps. We're talking 100-1000 lines of proof per line of program code.

I don't know when AI will be able to do all that, but I see no reason to believe that a computer that can do that wouldn't also be able to reconcile the formal statements of correctness properties with informal requirements, and even match the requirements themselves to market needs.

Re: Test, don't just verify

#98

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…

> A static type check doesn't stand in for "a" unit test; static typing stands in for an unbounded number of unit tests.

You have conflated "a static type check" with "static typing". Unit tests stand in, in the same way, for an unbounded number of states of real-world input. They're simply being subjected to a trial verification system rather than a proof system. It turns out that writing proofs is not very many people's idea of a good time, even in the programming world. And the concept of "type" that's normally grokked is anemic anyway.

> Put another way...

Rhetoric like this is unconvincing and frankly insulting. You pass off your taste and opinion as fact, while failing to understand opposed arguments.

Re: Test, don't just verify

#99
post #80

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…

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…

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

My experience is radically different. `ValueError` is far more common in my un-annotated Python, and the most common cause of `TypeError` anyway is the wrong order or number of arguments after a refactoring.

Re: Test, don't just verify

#100
post #78

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!

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 expect any of it to be applicable to Python. This is why the Haskell people speak of dynamically-typed languages in the Python mold as "untyped" regardless of their attitude towards implicit casts.

And I love it, and have been using it for decades, and write beautiful things where the annotations hardly ever seem worth the effort — perhaps for documentation, but not for a static checker. Then I look at other, newer Pythonistas trying to figure out how to write complex generic type expressions (and sacrificing backwards compatibility as they keep up with the churn of Python figuring out how to offer useful annotation syntax) and deal with covariance vs contravariance etc. and I just smile.

Post reply on HN