>>3
one part of my brain agrees, but ...
other part of my brain thinks :
do you really like to write correct proof code yourself (& enforce it on everyone else) (& how big is portion of correct software overall being written & used) where:
1+1=2
requires a proof that 1 & 1 are Natural numbers & positive, non-negative Integers & not Floats or Doubles or chars (but could be bits). A bits that are opposite of (!=) 0 (e.g. not equals (which is revert condition)).
...
etc
There is whole 3 volume book Principia Mathematica from 1912 that spend 360 pages proving 1+1=2.
or, life is short, you write MVP in any practical language of you choice, maybe even ASM, maybe with few small bugs like everywhere, that will be payed to be fixed not by you, you sell your MVP Startup to Google, for 100M. You spend money to meaningful things like donating to FLOSS, offering sposorhip grants for some ones Homotopy type theory research, paying for healthcare of you fam.
e.g. before writing a correct code, heck, even before learning how to write safe correct code, you have to answer one single most important question in Computer Science formulated by Dr.Terry Davis.