4 ms·

I've heard of those, but I don't think I quite know what they are for. Formally proving things about a program sounds cool, but what are some practical applicat

• staunton 3y ago
  For example, making "exhaustive tests" (as if you're able to check every single possible user input), eliminating a lot of security vulnerabilities, provably correct implementations of cryptographic algorithms (DJB is playing with Lean a lot right now and wrote a paper on what it's like), being able to reason better about the program, composing different programs while maintaining these advantages. The "reason" why people ask "what's the use of that" is that they just assume that writing bug-free and correct software is impossible and not worth trying.
  • catlover76 3y ago
    Oh cool