[ebingdom]

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?

[mikedodds]

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.

[userbinator]

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.

[mecsred]

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.

[zmgsabst]

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/

[HWR_14]

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?

[mrslave]

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/

[jnash]

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.