Crazy ambitious. I don't doubt that Unison could be very nice, but I wonder about that assumptions. How much of the state of programming is due to legacy, and how much is due to human nature and the need for complexity and adaptability? In the end Unison's approach will necessarily reflect one set of choices that another group of devs would not make.
Full disclosure: I know nothing about programming. To me, this seems like the probable outcome of this: Am I incorrect? I feel like a better use of programming time would be to create some sort of shell which you could lay over an existing programming language to do what Unison is supposed to do.
Just to tack on to your point, it applies especially well when it comes to semantic editors. I quote a comment from an article referenced in the linked page:There are serious problems with this vision of "always correct by construction". Often, "work in progress" is in an inconsistent or amorphous state and that needs to be represented somehow. Programmers, mathematicians, musicians, dancers, writers are all involved in creative activity in which being shackled by rules, even the ones one wants to apply at some point, can reduce flow. So I believe there will always be a need for after-the-fact validation, correction, refactoring.