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 propertie

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