Hacker News new | past | comments | ask | show | jobs | submit login
Practical Proofs: Proof Approximations for Practical Code (zerobugsandprogramfaster.net)
41 points by kiyanwang on Oct 24, 2016 | hide | past | favorite | 17 comments



Bravo to Ms Thomson for championing this kind of thinking. I also like her choice of languages -- m4!

Still I wish the write-up spelled out her thinking more. I think her two examples are supposed to be positive here-is-how-you do it cases. But then she immeditaely says they could be better, and even points out a serious problem with the second example.

The biggest thing though is culture and process: it's great to have style for leaving comments to your co-workers about restrictions and guarantees. But in the wrong work environment, those comments will be ignored. What I want to know is how to build the right environment.


> But in the wrong work environment, those comments will be ignored. What I want to know is how to build the right environment.

Hiring the right people is the hard part. Or (better) not hiring the wrong people.


I think her two examples are supposed to be positive here-is-how-you do it cases. But then she immeditaely says they could be better, and even points out a serious problem with the second example.

I did it that way to help get people into the habit of immediately looking at their code after they write it and see if there is anything that can be improved :)


We are all born not knowing how to program.

We were all lousy programmers at one time.

We can all learn to do better. Teach your coworkers.


All of my co-workers are good programmers. But some are good programmers who care about invariants and others are good programmers who will trample invariants to get this week's feature done.

I think it is really a matter of process. E.g. code reviews. But I don't yet know how to strike the balance between rigour and efficiency.


others are good programmers who will trample invariants to get this week's feature done.

That doesn't sound like good programmers tbh


This is what objects were supposed to be for. When you have some consistency requirement between some variables, you make them private to an object and only export methods which maintain that consistency requirement.

Somehow this seems to have been lost.


Objects coupled with formal proofs, maybe.

Otherwise, nothing has been lost: naïve approach to objects seems to work well for managing memory and garbage collection, otherwise it's just a bothering implementation detail of a language runtime, that does not help a programmer much and is itself a liability.

Objects do dynamic checks at runtime, whereas types are known (and verified) before a program is executed.


That is a good idea as far as it goes, but it does not go far enough. Soon enough you will find a consistency requirement that does not fit into any structure that works for other consistency requirements (other than the degenerate God object antipattern, which defeats the purpose) - and consistency is only the first step to being correct, anyway.


Has anyone read the actual book mentioned in the blog? Opinions?


So... what would an example informal proof look like?



Which browser?


Latest firefox, ubuntu


Thanks! I fixed it (I don't have Ubuntu Firefox to test, though).


Thanks, really.


Fix confirmed :)




Consider applying for YC's Summer 2025 batch! Applications are open till May 13

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: