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

41–50 of 146 posts

Re: Test, don't just verify

#41

Post by packetlost »

brabel wrote: post #37
packetlost wrote: post #32

Earlier quoted context omitted.

I think it's possible to write correct systems with dynamic languages, just not the ones we commonly use like Python and JavaScript. I find Clojure, for example to be one example of a dynamic language that is pretty easy to manage and I attribute that to the immutable nature and data-centric ethos. I'm sure there are other dynamic languages that would work as well. Now, I wouldn't necessarily use Clojure on a huge mu…

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 haven't done much with CL so I can only speculate, but I think stricter FP principles in general work to minimize the downsides of dynamic typing. CL, to my understanding, isn't the most "pure" when it comes to FP, but does a good job at giving the programmer a lot of power to constrain and explore systems.

Re: Test, don't just verify

#42

Post by lesuorac »

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…

If you care about the type of a parameter you can just add an assertion in the method /s

Re: Test, don't just verify

#43

Post by loglog »

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…

The author is in the comfortable position of working on a system that does have a formal specification and a formally verified reference implementation. The post is not about how they wish things would work, but how their existing system (Cedar) works.

Regarding your point on Rust, the vast majority of software has nowhere near the amount of static guarantees provided by Rust. If you need more, use static memory allocation, that's what people do for safety critical systems. By the way, it seems that Rust aborts on OOM errors, not panics: https://github.com/rust-lang/rust/issues/43596

Re: Test, don't just verify

#44

Post by seg_lol »

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…

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.

Re: Test, don't just verify

#45

Post by xp84 »

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 certain requirements that all have correct outputs? Won’t many of these be terrible in terms of performance, time complexity, etc? I know that in the most trivial case, AI doesn’t jump straight to O(n)^3 solutions or anything, but also there’s no guarantee it won’t have bugs that degrade performance as long as they don’t interfere with technical correctness.

Also, are we also pretending that having Claude spin for “even weeks” is free?

Re: Test, don't just verify

#46

Post by layer8 »

altmanaltman wrote: post #30
9rx wrote: post #27

Earlier quoted context omitted.

Trouble is that TDD, and formal proofs to much the same extent, assume a model of "double entry accounting". Meaning that you write both the test/proof and the implementation, and then make sure they agree. Like in accounting, the assumption is that the probability of you making the same mistake twice is fairly low, giving high confidence to accuracy when they agree. When there is a discrepancy, then you can then unp…

I don't fully understand what you mean by accounting expects the probability of making the same mistake twice is fairly low? Double-entry bookkeeping can only tell you if the books are balanced or not. We absolutely cannot assume that the books reflect reality just because they're balanced. You don't need to mess up twice to mess up the books in terms of truthness. Also tests and code are independent while you always…

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 is a very different kind of error than having an error in the implementation of that property. You don’t have to make the “same” error on both sides for an error to remain unnoticed. Compared to bookkeeping, a single random error in either the tests or the implementation is more likely to remain unnoticed.

Re: Test, don't just verify

#47

Post by hun3 »

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…

Verified software should satisfy the liveness property; otherwise, an infinite loop that never returns would pass as "correct."

Verifying realtime software goes even further and enforces an upper bound on the maximum number of ticks it takes to complete the algorithm in all cases.

Re: Test, don't just verify

#48

Post by layer8 »

TeodorDyakov wrote: post #25
smccabe0 wrote: post #15

Earlier quoted context omitted.

I think the section on AI from Zero to QED (a proofs in Lean/lang guide) gives a sober path forward from the perspective of market-makers and trading: "Imagine market infrastructure where agents must prove, before executing, that their actions satisfy regulatory constraints, risk limits, fairness properties, and eventually machine-checkable proofs of Pareto efficiency of market mechanisms. This is a big, hairy, ambit…

I dream of a future where before any software is released we can predict 100 years into the future what effect it will have on every living thing and not release it if unhappiness delta for some living thing falls below a certain threshold.

That would require making the behavior of the living things part of the formal specification, which isn’t really possible.

Re: Test, don't just verify

#50

Post by gaogao »

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…

Yeah, Rust has been pretty good for formal verification so far. Hoare spec contracts I think are the way forward, especially since they fairly naturally flow from unittests. I've been using Hax to pretty good effect so far. I'm generally suspect that advances in Lean proof solving by dedicated models are that useful for program verification, compared to generalist models, though it could help lower costs a good bit.
Post reply on HN