Oula, quand je faisais du Coq, c'était un petit peu plus simple
Oh si.
Plutôt qu'une preuve, on fait voter tous les coeurs et on compte les résultats.
Je -> []
Pas que je sache, mais techniquement, je pense que ça pourrait. Il y a quelques papiers sur la parallélisation du moteur de typage de Haskell, donc pourquoi pas celui de Coq. Il y a aussi des tactiques brute-force dont la recherche pourrait surement être parallélisée.
Pour rappel, voici les principales tactiques de Coq, et leur traduction en maths :
Trivial.Code:trivial.
Par un calcul évident.Code:simpl.
Preuve calculatoire simple, omise.Code:omega.
Démonstration laissée en exercice.Code:auto.
Par application d'un théorème de Gauss.Code:auto with *.
Voir preuve dans la marge.Code:intuition.
"Disclaimer
Your life is always more valuable than any code. You should leave the building immediately in a true emergency.
Code can be re-written, but humans cannot."
Mais bon après ça dépend y'a des pertes acceptables
à mes débuts, quand on ouvrait le shell on avait toujours un petit conseil à la con (me souvient plus de la commande).
Un jour il m'affiche "The world is coming to its end. Save your buffers".
Ça m'avait fait marrer.
...
Il y a trente ans
Y'avait pas un /etc/motd, pour "message of the day"? (vieux souvenirs de bidouilles config sur une version de Linux pre-v1...)
ça piochait une ligne random dans un fichier text... c'est un peu vieux
C'etait pas la commande "fortune" ou "luck" ?
Ah je dis pas que c’était hyper subtil, hein. Mais y'avait un lot de trucs marrants...
Sur l'Internet, il y a aussi le port 17 qui est dédié à ce service de base :
https://tools.ietf.org/html/rfc865
(oui, c'est la spec complète)
C'est le protocole idéal pour les exercices niveau hello world avec des sockets.
Comme je sais qu'on est quelques uns à utiliser Visual Studio ici, je voulais vous dire que j'ai publié un thème sombre que j'ai créé et utilise depuis quelques années. (vu que je ne trouvais rien qui me plaise vraiment dans les dépôts, et par défaut, le blanc arrache œil/thème brun dégeu, non merci).
A savoir que c'est inspiré du thème Spacegray pour Sublime Text, combiné avec le "color_scheme" nommé "Packages/Color Scheme - Default/Sunburst.tmTheme".
Bon je retourne faire de la nécromancie de mon coté (je suis en train de créer un PoC basé sur Electron + Angular 5 chargé dans un projet Node.js dans Visual Studio).
Vous pouvez me jeter des cailloux.
Vous me trollez là.
Le thème sombre de base est brun, pas noir : là j'ai un fond vraiment noir, et je préfère avoir des tons anthracite/bleu que vers le brun/jaune dégueu. (ça se vois que je suis tombé dans la programmation en venant du graphisme ? )
En haut : mon thème, en bas : le thème sombre par défaut :
Ça manque de couleurs tout ça.
En thème sombre Darkula (IDE) + Monokai (font) > all.
C'est la faute à Arteis