4 ms·

That is a great counter example. I expect there to be a slow migration to platforms like [this formally verified microkernel](https://sel4.systems/ https://sel

That is a great counter example. I expect there to be a slow migration to platforms like [this formally verified microkernel](https://sel4.systems/ 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.

pitay 9y ago
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.
- lilott8 9y ago
  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 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.

pitay 9y ago

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.

lilott8 9y ago
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 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.