Depends on the constraints you want to prove that the program will uphold. Some constraints may be impossible to prove, especially in non-real time contexts.

For example, a program must run on a platform that doesn't have everything formally defined or have guarantees. If a program relies on that platform and that influences the program in a way that makes the constraint reliant on the platform, then you are out of luck.

Another issue is choosing the constraints that the program will operate under. You would hope that the clients would give you the requirements including the constraints the software must operate under. But this isn't often the case. Having an incremental approach which includes clarifying requirements by mapping what the clients need to do to get their work done, which includes recording the specific steps that they perform or need to perform works pretty well when clients don't provide the requirements or constraints upfront.

I am relatively ignorant on formal engineering, but I do like that you have provided a fairly clear definition, which was "Clearly define the constraints in which your project will operate under and prove that they will hold under those constraints". It is better than the people saying know more math, without saying how, or what, or why it is useful in any clear way, and saying software is math just doesn't cut it.

That is a great counter example. I expect there to be a slow migration to platforms like [this formally verified microkernel](https://sel4.systems/). This will take time and a tremendous amount of effort. But will ultimately address the counter example. In the conclusion of this migration, this puts the SE field into line with the rest of engineering.

Choosing the constraints for a project is no different in the context of CS than the context of any other fields -- electrical, mechanical, etc. It is a conversation, as you stated. This helps in many ways: it helps the developer understand exactly what the client wants, helps the client understand exactly what they are going to get, and helps build an implicit timeline replete with discrete and obvious deliverables and (if done correctly) those deliverables are fairly modular.

Thanks! I, too, get frustrated that people just say 'math! math! math!' That isn't helpful or meaningful. This is a conclusion I came to after talking to quite a few of my friends and colleagues in different engineering disciplines.

Thanks for the information, it is very much appreciated. I was a little frustrated that comments on this thread had people saying you should learn the math and prove your programs but providing no information on how to do so. It would be great if provided resources to show people how to do it. Or even better, provide a project that they worked on and show how they used formal methods to move through the project in detail, which would be wonderful. If someone wants to promote formal methods, then should not just argue for it, but teach it, even a tiny bit. That would get a way better reception.

A little off topic, but it would be great if there was a method/system which could provide requirements tracking down the set of artifacts to where you could point to a bit of source code and say it implements that certain requirement. Sort of like a chain of responsibility for code and associated documents. That might be a pipe dream, I don't know.

Anyway, thanks for the information, I remember seL4 being mentioned in discussion of the sorry state of software on medical devices, but had forgotten it until you mentioned it. Thanks.

To address your specific concerns regarding "learning the maths": that's a bit disingenuous from the people stating it. It is actually logic they are talking about, rooted in the discrete math branch. For seL4 you can actually read the proofs and their conclusions: http://sel4.systems/Info/FAQ/proof.pml. It's a lot of (structural) induction style proofs. That page will be a good starting point and just google around for missing holes as you need.