(My) Intro To Formal Methods
Published:
Over the last two years at Brown, I’ve taken a few courses in Formal Methods a subfield in Computer Science that touches upon multiple areas of theoretical computer science.
Broadly speaking the field is concerned with mathematical verification of software and hardware specifications. This also extends into other cool things like proof assistants (math on computers) and program synthesis (generate code).
I’ve found these courses fun and interesting and TA’ed two courses (CSCI1951X , CSCI1710) my sophomore year.
My motivation for writing this post is based on:
- I find this really cool and I think the importance of these methods is going to grow.
Most fellow CS undergraduates I talk to are unaware of the existence of the field. Everyone’s heard of databases,systems,cryptography and understand what those fields involve even if they haven’t taken any courses in that area. However formal methods (FM) has a bit of a PR problem :
- It’s not a core requirement in undergrad programs
- Most people’s brush with theory is through intro to discrete math (CS0220 at Brown) which they dislike.
- while FM has applications in distributed systems, cryptography etc , courses in those areas usually don’t cover verification techniques.
- A vast majority of software engineers do not directly work with the tools/techniques of FM
- it’s not cool/sexy like machine learning
To address this deficit I intend to cover here :
- Why Verification
- Satisfiability Solvers
- Proof Assistants
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.