Verified software development in Lean

Over the past year, the Lean FRO has been mak­ing a big push to­wards mak­ing Lean a great gen­er­al-pur­pose pro­gram­ming lan­guage that you can use to de­vel­op for­mal­ly ver­i­fied pro­duc­tion-ready soft­ware. In this pre­sen­ta­tion, I will give an overview over the many re­cent in­no­va­tions in Lean that are rel­e­vant for soft­ware de­vel­op­ers, in­clud­ing im­prove­ments to the com­pil­er, the stan­dard li­brary, and the ver­i­fi­ca­tion in­fra­struc­ture for monadic pro­grams.