A focus on soundness does not, I believe, help the cause of more correct software but distracts from techniques that have proven more fruitful in practice (and supported by theory) -- sometimes to the surprise of those who used to think that soundness is the only way, e.g. http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h.... This happens over and over: there is some important improvement in sound methods while at the same time unsound methods are making much bigger strides toward more correct software in practice. Here's just one very recent example (which isn't even necessarily state-of-the-art in unsound methods): https://antithesis.com
Of course, this is a very complex topic, because there are some specific situations where sound techniques are more powerful and practical.
Which kind of touches on the other problem, which is the difficulty of getting people to even use the easy, low-cost techniques we already know. Here we are talking about SAT solving and formula propagation and how unsafe Rust interacts with those things and in the world I experience a moment of shock if I so much as see
type Username string
type Password string
func Login(Username, Password)
instead of
func Login(username string, password string)
in code. (Obviously these type signatures are just complex enough to make my point and would generally have more to them in the real world.)
Or at times even just encountering a unit test is enough to surprise me. Programmers need to get really, really tired of fixing the same bug(s) over and over in QA before they finally have the brainwave of adding their first unit test somewhere around the 25,000 line point.
I wish formal methods all the best and I wish I had more time to spend with them, but I'm awfully busy fighting upstream just to keep the unit tests running every time a new developer joins the project. I'm just asking for you to please install the git precommit hook or actually pay attention to the CI or whatever. Please. I'm not asking you to learn a SAT solver. Just keep the tests passing, and if a test broke because it's no longer applicable, please remove it instead of just letting it break for the next couple of years. etc.
> before they finally have the brainwave of adding their first unit test somewhere around the 25,000 line point
In my experience the driver for this is "whoever has the money", not programmers. The programmer who carefully writes tests from line 0 gets laid off/told to speed up while the programmer who hacks together a bunch of janky code with no tests, but demos something cool to the <person with the money> is not laid off.
Only if the programmers are doing it wrong. I add unit tests from day one not because I'm just that disciplined... honestly I think my discipline may even be a touch sub-average compared to a lot of programmers... I add them from day one because they speed me up, starting somewhere around the third week or so (so we're not talking years before it pays off here). I do not understand how programmers are OK with making a change and then only finding out later that they broke something distant that they wouldn't have thought would break. It would be so frustrating. Or decide to refactor something in week 4 without unit test support.
Your janky code guy may beat me in the first month but after that I'm quite likely going to pass him and never look back.
Revealed preference of business is to move fast and break things. ("Any idiot can build a bridge, it takes a professional (an engineer!) to build one that barely stands.")
I grieve with you but it seems the way out of this is through some kind of magic potion cooked of the usual forbidden ingredients of: free and open source, being your own boss, idealism, etc.
It's not a bad idea to strongly type the username and password so that you can't so easily pass in unexpected input to the login / can centralize validation (e.g. username and password can't be more than 100 bytes each to attempt a login). It also lets you implement things like secure erasure of the password once it gets dropped.
Weakly typing that though is a sin. I wish Rust made creating strongly typed wrappers around primitives a bit more ergonomic.
By any chance can you elaborate on a bit of what are these unsound methods are, what's the current state-of-the-art? And what antithesis does? (Is it a fuzzer?)
What does "unsound method" mean in this context? Doesn’t that mean, if it finds a bug that this may not actually be a bug? I.e. it may give false positives?
A focus on soundness does not, I believe, help the cause of more correct software but distracts from techniques that have proven more fruitful in practice (and supported by theory) -- sometimes to the surprise of those who used to think that soundness is the only way, e.g. http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h.... This happens over and over: there is some important improvement in sound methods while at the same time unsound methods are making much bigger strides toward more correct software in practice. Here's just one very recent example (which isn't even necessarily state-of-the-art in unsound methods): https://antithesis.com
Of course, this is a very complex topic, because there are some specific situations where sound techniques are more powerful and practical.
reply