Some notes on Rust, mutable aliasing and formal verification

Re:Some notes on Rust, mutable aliasing and formal verification by jerf on Thursday May 16, 2024 @09:38AM (#40378323)

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.

[ Parent | on HN ]

Re:Some notes on Rust, mutable aliasing and formal verification by dboreham on Thursday May 16, 2024 @10:37AM (#40379013)

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

[ Parent | on HN ]

Re:Some notes on Rust, mutable aliasing and formal verification by jerf on Thursday May 16, 2024 @11:43AM (#40379735)

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.

[ Parent | on HN ]

Re:Some notes on Rust, mutable aliasing and formal verification by pas on Friday May 17, 2024 @05:05AM (#40387869)

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.

[ Parent | on HN ]

Re:Some notes on Rust, mutable aliasing and formal verification by vlovich123 on Thursday May 16, 2024 @01:28PM (#40380917)

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.

[ Parent | on HN ]