Link - If It Compiles, It Is Correct

Link: If It Compiles, It Is Correct: A Practical Introduction to Lean 4 for Engineers

An introduction to Lean 4, a programming language that can be used to prove software correct.