Thanks for the awesome answer, with citations! As someone who has to do day to day programming in languages with minimal concept of safety (e.g. JavaScript, C)

Thanks for the awesome answer, with citations! As someone who has to do day to day programming in languages with minimal concept of safety (e.g. JavaScript, C), my concern isn't for provably correct, it's for "make my life easier by covering the 90% case." Number of times I've needed to work with 255 bit integers: 0. Number of times I've confused units of time passing into APIs: way too many. Heck on one system I was working on, I had one API that took distance in as thousands of an inch. Everything else was in metric. Fixing that sort of stuff could be done w/o great trouble, and it'd be a huge boon to everyday programmers. Would it be a sexy language feature? No. But it'd make life better.