I'd love to hear a little bit more on what you think the downsides are? (Or a recommendation for a resource to read up on this?)

Add-on story:

I joined binwiederhier for a while in developing Syncany and he invited me for an internship at his current employer.

The experience I gained both in contributing to Syncany and said internship helped me indirectly land the role I'm currently in, and my open source experience in general helped me land a cool engagement where I got to do some innovative open source projects.

Not strictly what you're looking for, but in Lean (functional language/theorem prover), there's some interesting work being done. Using the tool actually shows which suggestions will compile, which certifies correctness to some degree. https://leandojo.org/