Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Evolutionary couplings between files reveal poor software design choices

ergoso.me

Post reply on HN
Print view View original

81–85 of 85 posts

Re: Evolutionary couplings between files reveal poor software design choices

#81

Post by [deleted] »

evincarofautumn wrote: post #66
paulsutter wrote: post #63

> I was thinking about writing up a small application paper for this project, but I am really terrible at reading papers from the Computer Science field, let alone writing them. Thank goodness for that. This blog post was so much easier to read then a formal paper. Why are formal papers so tedious to read? Imagine how much time we'd waste as a group if he written this as a paper. Many of us would give up before findi…

I have found that the best papers are hard to read because they’re informationally dense, so you have to slow down to really process every sentence and unpack the author’s thinking in your head—but once you do, you get a lot of knowledge from just a few pages. So it ends up being worthwhile. Average papers are hard to read because they’re trying to emulate the style of the good papers, but without having enough actua…

[deleted]

Re: Evolutionary couplings between files reveal poor software design choices

#82

Post by chongli »

vertex-four wrote: post #80
chongli wrote: post #79

Earlier quoted context omitted.

If you have to write a formal proof, what's making sure the proof is actually proving what you intend? And what's the actual difference between this proof and the implementation? The formal proof is the implementation. It is the code you run in production. The proposition is your types. Instead of writing tests, you write types. It's the exact same process you would use with "red-green-refactor" TDD except it's the c…

I will certainly watch those - but for the moment, I see no obvious way to immediately see that a proof is proving what you intended it to prove, whereas `assert (append "foo" "bar") == "foobar"` immediately shows what you expect and can be read and checked by somebody with the slightest programming knowledge. The point of tests is that they're supposed to be simple enough that it should be near-impossible for them t…

You don't have to see that the proof is proving what you intend; the type-checker does that for you. This is why some people sometimes refer to type checkers as small theorem provers.

As for your assert example, how do you know append will work as you expect for all possible strings (including null characters or weird unicode edge cases)? With a proof you will know.

Re: Evolutionary couplings between files reveal poor software design choices

#83

Post by vertex-four »

chongli wrote: post #82
vertex-four wrote: post #80

Earlier quoted context omitted.

I will certainly watch those - but for the moment, I see no obvious way to immediately see that a proof is proving what you intended it to prove, whereas `assert (append "foo" "bar") == "foobar"` immediately shows what you expect and can be read and checked by somebody with the slightest programming knowledge. The point of tests is that they're supposed to be simple enough that it should be near-impossible for them t…

You don't have to see that the proof is proving what you intend; the type-checker does that for you. This is why some people sometimes refer to type checkers as small theorem provers. As for your assert example, how do you know append will work as you expect for all possible strings (including null characters or weird unicode edge cases)? With a proof you will know.

> With a proof you will know.

But I could just as easily accidentally write a proof which proves something else, couldn't I? This is complex code expressing complex ideas - a type system would certainly help, but it can't tell me that I'm proving the wrong thing.

Re: Evolutionary couplings between files reveal poor software design choices

#84

Post by chongli »

vertex-four wrote: post #83
chongli wrote: post #82

Earlier quoted context omitted.

You don't have to see that the proof is proving what you intend; the type-checker does that for you. This is why some people sometimes refer to type checkers as small theorem provers. As for your assert example, how do you know append will work as you expect for all possible strings (including null characters or weird unicode edge cases)? With a proof you will know.

> With a proof you will know. But I could just as easily accidentally write a proof which proves something else, couldn't I? This is complex code expressing complex ideas - a type system would certainly help , but it can't tell me that I'm proving the wrong thing.

But I could just as easily accidentally write a proof which proves something else, couldn't I?

Then your proof would be rejected by the compiler. Remember, the types specify your proposition: i.e. what you are intending to prove. The actual proof itself is the function you implement for that type.

As for whether you're proving the right thing or the wrong thing, a type system is no less helpful than a test suite. The advantage of a type system is that it checks whether your types are consistent within the entire program rather than in merely the specific test you're running.

Re: Evolutionary couplings between files reveal poor software design choices

#85

Post by vertex-four »

chongli wrote: post #84
vertex-four wrote: post #83

Earlier quoted context omitted.

> With a proof you will know. But I could just as easily accidentally write a proof which proves something else, couldn't I? This is complex code expressing complex ideas - a type system would certainly help , but it can't tell me that I'm proving the wrong thing.

But I could just as easily accidentally write a proof which proves something else, couldn't I? Then your proof would be rejected by the compiler. Remember, the types specify your proposition: i.e. what you are intending to prove. The actual proof itself is the function you implement for that type. As for whether you're proving the right thing or the wrong thing, a type system is no less helpful than a test suite. The…

> Then your proof would be rejected by the compiler.

Only for some types of mistake, surely. If that was always the case, we'd have a compiler that could read minds.

> As for whether you're proving the right thing or the wrong thing, a type system is no less helpful than a test suite.

Really? I can write down in my test suite, "assert (add 1 1) == 2". Anyone can come along and look at that and make sure it matches the spec. We can add additional tests for various bounds, and possibly use a quickcheck-like tool in addition, and for 99.99% of use cases be happy and confident that we're at least writing the right thing.

What's the type for that and does it actually have any resemblance to "the add function adds two numbers together", or do I have to read a couple of papers and have a background in university-level math to convince myself that the proof actually does what it says?

Post reply on HN