5 ms·

In CS212 we're mostly writing simple recursive programs in SML and proving using induction that they evaluate to the correct result. We step through the program

In CS212 we're mostly writing simple recursive programs in SML and proving using induction that they evaluate to the correct result. We step through the programs by hand on paper. This seems very different, and I'm wondering if what we're learning has any practical application.

mistrial9 6y ago
IMHO your CS212 work is didactic, not applied
strangecasts 6y ago
Not familiar with that course, but there are definitely applications for proof-writing to show that code does what you expect and/or satisfies certain properties - the seL4 microkernel [1] is probably the highest-profile example - but it quickly becomes impractical beyond small programs, or if the code wasn't written with proving in mind initially. IMO the most "practical" application for those methods is in strengthening type systems to allow more expressive constraints - one small example that comes to mind is Idris [2] allowing you to explicitly mark certain functions as total [3] and fail type-checking if they don't return a value for every possible input. The main thing to keep in mind with TLA+ is that it's not really meant for validating code, it's more for showing that your design is consistent and satisfies safety requirements (e.g. "no temporary node failure should result in data loss"). However, having a TLA+ specification usually makes the implementation fairly straightforward, especially in languages/environments with message-passing concurrency. You can use TLAPS [4] to write proofs-by-induction similar to yours for TLA+ specifications, but IMO the real power is in model-checking them with TLC, which gives you a lot of the advantages of formal methods with much less proof work. [1] https://github.com/seL4/l4v https://github.com/seL4/l4v [2] https://www.idris-lang.org/ https://www.idris-lang.org/ [3] https://idris.readthedocs.io/en/latest/tutorial/typesfuns.html#totality https://idris.readthedocs.io/en/latest/tutorial/typesfuns.ht... [4] https://tla.msr-inria.inria.fr/tlaps/content/Home.html https://tla.msr-inria.inria.fr/tlaps/content/Home.html
remexre 6y ago
That's a different style of proof, based on equational reasoning; Agda [0], Coq [1] and Lean [2] are three theorem provers that work with those proofs better. Being able to quickly and informally perform equational reasoning on functional programs is also what (imo) makes those languages easier to think about, so it's a valuable skill outside of proving. [0]: https://wiki.portal.chalmers.se/agda/pmwiki.php https://wiki.portal.chalmers.se/agda/pmwiki.php [1]: https://coq.inria.fr/ https://coq.inria.fr/ [2]: https://leanprover.github.io/ https://leanprover.github.io/
alphakilo 6y ago
In my school our Software Eng program is heavily focussed on formal verification. In my experience, the practical applications we learn are still too fat detracted from industry to be applicable. Everything starts with two logic courses EECS/MATH 1028 which covers basics like induction and pigeon hole princele and MATH 1090 which covers first principles and axioms of logic. Then, using the courses on logic that we did by hand, we have a system verification course (EECS 3342) with SMTs like Rodin which can solve on its up to a point where we need to manually input the proofs. Beyond this, we also cover proving preconditions and post conditions through design by contract in EECS 3311 - Software Design (which is usually tough in Eiffel, but finally being taught in Java after a year of lobbying the faculty). Then our final courses are EECS 4312 and 4315 for requirements engineering and mission critical systems respectively. In 4312 we learn TLA+ and 4315 is focussed on tree and path logic for states. As well, we have EECS 4313 advanced software testing which is primarily about writing bug reports, creating tests (JUnit) and touches on distributed systems tests a bit. The point is that we do learn the "practical" (quite impractical since our prof's are not in industry) only once we have had a lot of exposure to proving things by hand. But even once we have learned everything, they fail to connect material to realistic SDLCs and how to implement the tools in an agile methodology.
Gene_Parmesan 6y ago
What you will realize years after you leave college is that in many cases, the way you do things is designed to get you to integrate a concept with your understanding of the domain. For instance, this is why many courses will ask you to write code to do something while disallowing the standard library. I see a lot of students complain "There's a library function that does exactly this but for some reason I can't use it!" But not using it is exactly the point. Viewing college as a trade school is a mistake many of us make. No, you're almost certainly never going to be manually proving things by induction in the real world. But that doesn't make the exercise valueless.

mistrial9 6y ago

IMHO your CS212 work is didactic, not applied

strangecasts 6y ago

Not familiar with that course, but there are definitely applications for proof-writing to show that code does what you expect and/or satisfies certain properties - the seL4 microkernel [1] is probably the highest-profile example - but it quickly becomes impractical beyond small programs, or if the code wasn't written with proving in mind initially. IMO the most "practical" application for those methods is in strengthening type systems to allow more expressive constraints - one small example that comes to mind is Idris [2] allowing you to explicitly mark certain functions as total [3] and fail type-checking if they don't return a value for every possible input. The main thing to keep in mind with TLA+ is that it's not really meant for validating code, it's more for showing that your design is consistent and satisfies safety requirements (e.g. "no temporary node failure should result in data loss"). However, having a TLA+ specification usually makes the implementation fairly straightforward, especially in languages/environments with message-passing concurrency. You can use TLAPS [4] to write proofs-by-induction similar to yours for TLA+ specifications, but IMO the real power is in model-checking them with TLC, which gives you a lot of the advantages of formal methods with much less proof work. [1] https://github.com/seL4/l4v https://github.com/seL4/l4v [2] https://www.idris-lang.org/ https://www.idris-lang.org/ [3] https://idris.readthedocs.io/en/latest/tutorial/typesfuns.html#totality https://idris.readthedocs.io/en/latest/tutorial/typesfuns.ht... [4] https://tla.msr-inria.inria.fr/tlaps/content/Home.html https://tla.msr-inria.inria.fr/tlaps/content/Home.html

remexre 6y ago

That's a different style of proof, based on equational reasoning; Agda [0], Coq [1] and Lean [2] are three theorem provers that work with those proofs better. Being able to quickly and informally perform equational reasoning on functional programs is also what (imo) makes those languages easier to think about, so it's a valuable skill outside of proving. [0]: https://wiki.portal.chalmers.se/agda/pmwiki.php https://wiki.portal.chalmers.se/agda/pmwiki.php [1]: https://coq.inria.fr/ https://coq.inria.fr/ [2]: https://leanprover.github.io/ https://leanprover.github.io/

alphakilo 6y ago

In my school our Software Eng program is heavily focussed on formal verification. In my experience, the practical applications we learn are still too fat detracted from industry to be applicable. Everything starts with two logic courses EECS/MATH 1028 which covers basics like induction and pigeon hole princele and MATH 1090 which covers first principles and axioms of logic. Then, using the courses on logic that we did by hand, we have a system verification course (EECS 3342) with SMTs like Rodin which can solve on its up to a point where we need to manually input the proofs. Beyond this, we also cover proving preconditions and post conditions through design by contract in EECS 3311 - Software Design (which is usually tough in Eiffel, but finally being taught in Java after a year of lobbying the faculty). Then our final courses are EECS 4312 and 4315 for requirements engineering and mission critical systems respectively. In 4312 we learn TLA+ and 4315 is focussed on tree and path logic for states. As well, we have EECS 4313 advanced software testing which is primarily about writing bug reports, creating tests (JUnit) and touches on distributed systems tests a bit. The point is that we do learn the "practical" (quite impractical since our prof's are not in industry) only once we have had a lot of exposure to proving things by hand. But even once we have learned everything, they fail to connect material to realistic SDLCs and how to implement the tools in an agile methodology.

Gene_Parmesan 6y ago

What you will realize years after you leave college is that in many cases, the way you do things is designed to get you to integrate a concept with your understanding of the domain. For instance, this is why many courses will ask you to write code to do something while disallowing the standard library. I see a lot of students complain "There's a library function that does exactly this but for some reason I can't use it!" But not using it is exactly the point. Viewing college as a trade school is a mistake many of us make. No, you're almost certainly never going to be manually proving things by induction in the real world. But that doesn't make the exercise valueless.