¿Existe una definición CS formal de VCS y versiones de archivo?

No sé si fue una broma, pero una vez que leí lo que se conoce como una definición formal de un archivo en un sistema de versiones como git, hg o svn. Era algo así como un objeto matemático como un homeomorfismo. ¿Fue una broma o hay realmente una teoría de la informática sobre los sistemas de versiones y las matemáticas de VCS?

Estás pensando en un tweet de Isaac Wolkerstorfer (@agnoster) :

git se vuelve más fácil una vez que se tiene la idea básica de que las ramas son endofunctores homeomórficos que mapean submanifolds de un espacio de Hilbert.

Lamentablemente, es una broma. Como el autor escribió en Quora :

Fue pensado como firmemente irónico. De hecho, amo a git, y creo que su complejidad es exagerada. Al mismo tiempo, simpatizo con el hecho de que los consejos de los git gurus a los novatos pueden terminar sonando como un galimatías inescrutable.

No tiene la intención de tener un significado más profundo. Los intentos de analizarlo de esta manera deberían ser inútiles, pero debido a un error en la realidad, puede hacer que cualquier declaración lo suficientemente ondulada a mano si se esfuerza lo suficiente.

Esto se ha discutido en Programmers Stack Exchange y en Mathematics Stack Exchange .

Broma a un lado, ha habido trabajo de formalizar el control de versiones. Un esfuerzo que alía la teoría y la práctica es el trabajo sobre la teoría del parche de David Roundy sobre Darcs . El objetivo principal de la teoría es modelar la fusión y, en particular, la resolución de conflictos. El wiki de Darcs tiene una introducción a la teoría y algunos consejos, así como una bibliografía (sin mantenimiento, así que está desactualizado si desea una visión reciente sobre el tema, pero contiene una encuesta de 2009 de Petr Baudiš ) y una lista de charlas ( que incluye material más reciente). También hay un wikibook . Un artículo seminal es Un enfoque basado en principios para el control de versionespor Andres Löh, Wouter Swierstra y Daan Leijen3 .

La teoría del parche conduce a un modelo categórico, que ha sido explorado más recientemente en A Categorical Theory of Patches por Samuel Mimram y Cinzia Di Giusto y Homotopical Patch Theory por Carlo Angiuli, Ed Morehouse, Daniel R. Licata y Robert Harper . En el trabajo de Mimram y Di Giusto, el modelo tiene archivos como objetos y parches como morfismos. Creo que eso hace que la fusión de una rama sea un functor, un endofunctor si está trabajando en un único repositorio. "Endofunctor homeomórfico" no tiene sentido para mí. Con la teoría de la homotopía involucrada, los submanifolds de un espacio de Hilbert podrían no estar tan lejos ...

Por supuesto, existe un formalismo matemático para los sistemas de control de versiones. Existe un formalismo matemático para prácticamente todos los algoritmos en CS. Hay múltiples formalismos para muchos. No existe una relación 1-1 entre formalismos y los sistemas que modelan . Los modelos pueden variar de simples a complejos. Aquí hay un ejemplo para VCS / SCM también de Swierstra, aún no citado.

• La semántica del control de versiones

SCM también tiene muchas similitudes con el concepto de "universos / líneas de tiempo paralelos" y el viaje en el tiempo a veces utilizado en la ciencia ficción. Captura el estado del sistema en evolución en diferentes momentos o "instantáneas". Hay "ramas" y "fusiones". Ver también cronogramas .