I imagine the burden will be mitigated by not requiring everyone to have the same level of expertise. The model I see is an architect using the type and proof s

I imagine the burden will be mitigated by not requiring everyone to have the same level of expertise. The model I see is an architect using the type and proof system to make a language that describes the problem domain at hand. It is this language that will be for the rest of the team. Now, will it look familiar? I would hope so.