So the "repo" in this case is a database, where currently the only things stored are denormalized source tree nodes. I could imagine extending the database to support arbitrary assets, probably also addressed by the hash of their contents (same as top-level language definitions are).
Oh hi kevin! So if there's a possibility that the "extra data" would get out of sync with the "source code" (e.g. via a git merge, or someone just editing the source code as plain text), then it unfortunately breaks the guarantees that this system needs :(
I guess I could store a sha of each and fail loudly if I detect that one was edited "outside of the IDE" but again I think that would break the assumptions that git makes about diffs &c.
I've tried to go down the "text but nicer" route before, and it always comes up short; so now I'm trying "text is not a supported representation" we'll see how far I get.
Hm so it is a state machine, but (my hope is that) all state transitions are simple and direct (and observable!) outcomes of user action. If the transitions get at all complex or unobservable, I'll probably call it a failed experiment.
It might also end up being the case that users keep types "visible" at all times, only turning them off in certain situations. I can also imagine a flag to "only hide inferred types that are primitives" or something similar.
So I think "easy to mentally model" gets harder and harder to achieve as the type system becomes more powerful. If your conclusion is that we keep the type system limited in power, that's valid! but not what I'm exploring.
Another point that I failed to make in the post (thanks for the pushback!) is that type inference algorithms leave you high & dry in the presence of a type error. Then you're left with lots of hidden state (the internal steps the algorithm took before arriving at the error) and the final conclusion, which, if you're lucky, points you to two places in the code where the inferred types are in disagreement.
With my proposed system, all types are annotated all the time (to be shown or hidden via editor flag, or on hover), and the annotations are updated in response to actions taken within the editor. The "algorithm" becomes extremely simple, with almost no intermediate steps.
Of course, proof will be in the pudding, if I can actually achieve a pleasant editing experience :)
Yeah, it is definitely nice to have inferred types surfaced to you, but in these systems they are still re-computed on every textual edit, as opposed to being "sticky" (persisted in the source tree).
Source control does look very different in a projectional language, as git diffs no longer make much sense (viewing a pull-request with the source tree's JSON blob is essentially useless).
Unison is the language that's gone farthest with this, as far as I know; their solution to diffs & merges is to handle everything from within their CLI, bypassing git entirely. I imagine I'll do something similar.
the difference here is that there's no "fake-world" contest. Tarsnap is asking for a real-world hack of their system.
Telegram, on the other hand, is trying to prove that their algorithm is unbreakable. AES is pretty good too.
As is noted in other comments, it's generally the system, not the algorithm, that gets broken.