11: {v : (IO ()) | v == Main.main}main = [Char] -> (IO ())putStrLn {v : [Char] | len v >= 0}"Easter Egg: to force Makefile"
Goal
Automatically Proving Properties of Programs
Verify: indices i, min are within bounds of arr
i
min
arr
Easy, use Program Logic + Analysis
No invariants? Inference via Analysis...
Invariants are Fixpoints of Reachable States
Computable via Dataflow Analysis or Abstract Interpretation
Imperative
First-Order Functions
Objects
Containers
Arrays, Lists, HashMaps,...
Polymorphism
Higher Order Functions
Verify indices i, min are within bounds of arr
Pose vexing challenges for Logic + Analysis
reduce
callback
Use Types to lift Logic + Analysis to Modern Programs
[continue]