Est-ce que l'algo seul peut être prouvé sans que le programme complet soit prouvé ? Je ne sais pas.
Ce n'est pas non plus ce qu'on demande aux autres (dont Git et Mercurial), mais j'avoue qu'on a hésité entre Rust et Idris à un moment, entre autres pour cette raison.
Si les algos sont prouvés, c'est déjà bien mieux que Git par exemple (en plus, quelle spécification donner à Git, vu qu'il fait parfois des bêtises ?).
Je veux bien aider des gens à le prouver, par contre, mais il faut commencer par les fondations (qui nous ont pris plus de temps que le projet lui-même). Exemples :
Sanakirja, un dictionnaire clef-valeur à la LMDB, mais avec des tables forkables efficacement (la complexité est compliquée à expliquer, je l'ai fait là). Le code n'est pas très gros, mais les algos sont un peu tordus : il y a des skiplists et des B trees, mais tout est transactionnel, y compris la gestion de la mémoire. Exemple, si on débranche la machine au milieu d'une transaction qui a alloué plein de blocs dans le fichier, quand on redémarrera, la base de données sera retrouvée exactement dans l'état initial (et Sanakirja n'a rien de spécial à faire, il n'y a pas besoin de journal, c'est seulement que le commit de transaction est atomique).
[^] # Re: Preuves ?
Posté par pmeunier . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 8.
Salut ! Je suis un des auteurs de Pijul.
Ce n'est pas non plus ce qu'on demande aux autres (dont Git et Mercurial), mais j'avoue qu'on a hésité entre Rust et Idris à un moment, entre autres pour cette raison.
Si les algos sont prouvés, c'est déjà bien mieux que Git par exemple (en plus, quelle spécification donner à Git, vu qu'il fait parfois des bêtises ?).
Je veux bien aider des gens à le prouver, par contre, mais il faut commencer par les fondations (qui nous ont pris plus de temps que le projet lui-même). Exemples :
Sanakirja, un dictionnaire clef-valeur à la LMDB, mais avec des tables forkables efficacement (la complexité est compliquée à expliquer, je l'ai fait là). Le code n'est pas très gros, mais les algos sont un peu tordus : il y a des skiplists et des B trees, mais tout est transactionnel, y compris la gestion de la mémoire. Exemple, si on débranche la machine au milieu d'une transaction qui a alloué plein de blocs dans le fichier, quand on redémarrera, la base de données sera retrouvée exactement dans l'état initial (et Sanakirja n'a rien de spécial à faire, il n'y a pas besoin de journal, c'est seulement que le commit de transaction est atomique).
Thrussh, une bibliothèque SSH asynchrone.