I find formal methods fascinating. To be able to say, no matter what the input is, this thing does exactly what it is supposed to do, is great. I wonder if one day we will be able to use a lighter version of formal methods to web development. I like the concept of Design by Contract, where you specify the pre- and post-conditions and invariants of a function, and it would already be a great step if it would be possible to prove the correctness of individual functions. Kind of the ultimate way of unit testing. I'm wondering how suited (or ill-suited) a language like Javascript is for applying formal methods on it. It's certainly not as "mathematically sound" as a language like Haskell, but then again, if it's possible to apply formal methods on C, then it should be possible to apply formal methods to Javascript too. I'm curious about research happening around this.