What, Why, and How of Formal Methods (2019)

Why don't people use formal methods? (2019) (HN)

F* - Verification system for effectful programs.

HOL Light - Computer program to help users prove interesting mathematical theorems completely formally in higher order logic.