Hacker News Reader

Comment by mbrodersen | Hacker News Reader

It’s great to see that proving code correct is starting to make inroads into commercial software development. Perhaps the term “Software Engineer” should be reserved for software developers who have the training/skills to formally prove software correct? The same way that Engineers in other industries have the formal training/skills needed to use mathematical models to build/construct correctly?

View on HN

As someone with years of experience writing machine-checked proofs in Coq, I cannot imagine the term "Software Engineer" shifting to that meaning, even though it may make sense when compared to other engineering disciplines. The programmers who have no experience with this technology outnumber us many thousands to one. They'd never sign off on it.

That said, I'm all for anything that results in more appreciation for mathematical rigor in programming. It's like puling teeth trying to get colleagues to use tools/languages that help with reasoning about code (even just a good type system), and for a lot of programmers math seems to be an unapproachable alien language.

One thing I'd like to change about the software industry is the perception that formal verification is too hard to do in practice because you can't even write down a complete specification for the program. The misconception there is that the all of the program's behavior needs to be specified in order for formal verification to be useful. Why can't gradual formal verification be a thing?

I wholly agree it’s important to contextualize formal methods — and particularly in terms of levels of rigor. Typing your program is already basic formal methods, and we do ourselves a disservice by using language which places proofs outside the realm of typing, testing, etc.

I think the “middle ground” between things like typing and things like fully specified programs are things like CDK apps which hook IAM policy or network reachability tools to analyze your infrastructure (and, eg, exclude open ports on the backend).

Which is slowly happening, eg AWS or Prime Video.

https://aws.amazon.com/security/provable-security/

I love math and a good type system. I know little about formal verification of code. Are there tools (ideally) or languages (for educational, if not production, use) you recommend I look at?

I went through Benjamin Pierce et. al - Logical Foundations [0] which uses Coq. It was great fun, and I am someone who has a pattern of shying away from mathematics a little too often. That said, I'm not the right person to tell you why and when Coq > all other proof systems. Pierce is famous though, and so are his books.

[0] https://softwarefoundations.cis.upenn.edu/

and for a lot of programmers math seems to be an unapproachable alien language

is the perception that formal verification is too hard to do in practice because you can't even write down a complete specification for the program

I think the main problem is that it's too formal. Turning something that is really about simple logical deduction into thick abstract maths is sure to dissuade the majority of the people who might find it useful. The elitist gatekeeping attitude that cryptographers tend to have doesn't help either.

A problem here is that it's not a simple logical deduction being converted to "thick abstract math". The math is the proof. A formal proof is necessary to verify the deduction.

Our approach for cryptographic systems is pretty much gradual verification. We target high risk or worrisome systems and verify piece by piece. It works! Formal verification is a relatively expensive technique so it's necessary (in my opinion) to target the places where you can achieve the best bang for buck.

For system reliability at scale, I think that stronger type systems and systematic testing techniques are probably the best choice. Anyway, that puts the system in a much better state if you want to apply formal verification later.

Can you elaborate a bit more on the kind of projects you have used Coq (and other tools) to prove correct? I am very much interested in moving in that direction career wise.

Some companies are using the title "Proof Engineer" to mean Software Developers that specialize in proving code/hardware correct. I think that's a great choice.

>Perhaps the term “Software Engineer” should be reserved for software developers who have the training/skills to formally prove software correct?

If I remember correctly my university used to offer a "software engineering" degree, which was a real engineering degree (in the sense you could take the professional engineer exam at the end of it) and had a number of common courses with the software development degree - the focus being on system engineering, low-level programming for embedded devices, and so on. I believe it was a mix of software dev and mechatronics or electrical engineering (?) and was aimed at students who wanted to work in medical, aerospace, and similar safety-critical fields.

But I can't see it listed on the current course offerings and suspect it has been discontinued - I think it was pretty unpopular due to the requisite math courses and generally having the same level of rigour as the other engineering degrees.

My university had a "school of computer science and software engineering" which was a joint school of the engineering department and the maths department.

Although the degree was very much a Bsc, I don't think getting a Beng was an option.

Reply on news.ycombinator.com