Add type engineering

content/docs/techniques/conditionals.md

@@ -1,6 +1,6 @@
 ---
 title: "Conditions" 
-weight: 2
+weight: 20
 ---
 
 # Conditions booléennes

content/docs/techniques/data-retrieval.md

@@ -1,6 +1,6 @@
 ---
 title: "Récupération de données" 
-weight: 1
+weight: 10
 ---
 
 # Récupération de données

content/docs/techniques/digging.md

@@ -1,6 +1,6 @@
 ---
 title: "Digging" 
-weight: 4
+weight: 40
 ---
 
 # Digging

content/docs/techniques/exercises.md

@@ -1,6 +1,6 @@
 ---
 title: "Exercices" 
-weight: 8
+weight: 70
 ---
 
 # Exercices

content/docs/techniques/loops.md

@@ -1,6 +1,6 @@
 ---
 title: "Boucles" 
-weight: 3
+weight: 30
 ---
 
 Il est possible de construire des boucles dans le cas où des étoiles

content/docs/techniques/permissions.md

@@ -1,6 +1,6 @@
 ---
 title: "Permissions" 
-weight: 6
+weight: 50
 ---
 
 # Permissions

content/docs/techniques/unit-testing.md

@@ -1,6 +1,6 @@
 ---
 title: "Tests unitaires" 
-weight: 7
+weight: 60
 ---
 
 # Tests unitaires

content/docs/type-engineering/_index.md

@@ -0,0 +1,5 @@
+---
+title: "Ingénierie logique" 
+bookFlatSection: true
+weight: 60
+---

content/docs/type-engineering/debug.md

@@ -0,0 +1,4 @@
+---
+title: "Mode debug" 
+weight: 50
+---

content/docs/type-engineering/effective-typing.md

@@ -0,0 +1,15 @@
+---
+title: "Typage effectif" 
+weight: 30
+---
+
+# Typage effectif
+
+Si on se contentait des spécifications idéales, on ne pourrait pas raisonner
+du tout puisqu'il faudrait souvent passer une infinité de tests.
+
+L'idée est donc de se contenter d'un ensemble fini mais suffisant afin de
+garantir un certain comportement. Une telle spécification est nécessairement
+partielle. Le critère d'orthogonalité doit aussi être calculable et tractable
+afin de garantir une vérification effective.
+

content/docs/type-engineering/ideal-typing.md

@@ -0,0 +1,68 @@
+---
+title: "Typage idéal" 
+weight: 20
+---
+
+# Typage idéal
+
+Le typage idéal (usage de Girard) n'apparaît pas directement dans le LSC,
+il s'agit plutôt d'un idéal intangible que l'on pourrait modéliser
+mathématiquement.
+
+Partons de la spécification. Nous voulons associer des étiquettes à des
+comportements que nous avons en tête. 
+
+## Définition par interaction
+
+On raisonne toujours par *interaction*, c'est-à-dire qu'on définit un concept à
+partir de l'ensemble des interactions associées.
+
+On doit tout d'abord définir un *critère d'orthogonalité*. Il s'agit : 
+- une relation binaire et symétrique entre constellations
+- d'une sorte de mesure de l'interaction entre constellations
+- d'un critère qui définit ce qui est considéré comme une interaction satisfaisante
+- d'un critère qui juge ce qu'est une interaction attendue
+
+Pour faire interagir deux constellations, il suffit d'exécuter leur union. On
+note `C _|_ C'` si les deux constellations `C` et `C'` sont *orthogonales*
+d'après un critère choisi, c'est-à-dire que l'exécution de `C + C'` satisfait
+le critère.
+
+Des critères possibles sont :
+- demander la terminaison de l'exécution
+- demander une constellation spécifique ou d'une forme spécifique en résultat
+de l'exécution
+- ...
+
+## Construction de spécification
+
+Soit **A** un ensemble de constellation. On note **~A** l'ensemble des
+constellations `C'` telles que pour toutes constellations `C` de **A**, on ait
+`C' _|_ C`.  
+
+Un ensemble de constellation est une *spécification idéale* si **A** = **~~A**
+ou de façon équivalente lorsqu'il existe un ensemble **B** tel que **A = ~B**.
+C'est-à-dire que **A** peut être caractérisé par interaction par un ensemble
+**B** vu comme une sorte d'ensemble de tests à faire passer pour affirmer
+l'appartenance à **A**. On cherche à avoir des objets *testables*.
+
+Il est évident que dans le cas général, ce **B** peut être infini et que donc
+on ne pourrait jamais affirmer en temps fini l'appartenance d'une constellation
+à une spécification idéale. Elles sont justement idéales en ce sens : elle
+capture parfaitement un comportement souhaité mais elles ne permettent pas
+d'étiqueter une constellation.
+
+## Exemple : fonctions
+
+On aimerait définir une étiquette associée correspondant aux fonctions unaires
+d'entier vers entier.
+
+On recherche un ensemble de tests : l'ensemble infini **Nat** de toutes les
+représentations d'entiers que de telles fonctions devrait pouvoir prendre en
+entrée.
+
+La spécification idéale recherchée est **Nat => Nat = ~Nat**.
+
+La difficulté est de trouver un critère d'orthogonalité et une représentation
+des fonctions cohérente avec cette notion de spécification. Ce n'est pas le cas
+de toutes les représentations imaginables d'entiers.

content/docs/type-engineering/orthogonality.md

@@ -0,0 +1,44 @@
+---
+title: "Définition d'orthogonalité" 
+weight: 40
+---
+
+<< En cours de construction >>
+
+Note : j'imaginais ici avoir un metalanguage permettant de définir une 
+relation d'orthogonalité par une constellation. On pourrait demander à ce que
+l'exécution de deux constellations testé par un critère d'orthogonalité renvoie
+`ok;`.
+
+Pour rendre les résultats d'exécution testables, on peut les envelopper avec
+un rayon `-test(...)`.
+
+J'avais en tête ce genre de syntaxe :
+
+```
+let ortho <ID-ORTHO> =
+  " definition de constellation
+end
+```
+
+Par exemple pour les automates qui renvoient `accept;` : 
+
+```
+let ortho <ID-ORTHO> =
+  -accept ok;
+end
+```
+
+On pourrait ensuite faire quelque chose du genre
+
+```
+let constellation c1 =
+  ...
+end
+
+let constellation c2 =
+  ...
+end
+
+test c1 c2 with <ID-ORTHO>
+```

content/docs/type-engineering/release.md

@@ -0,0 +1,4 @@
+---
+title: "Mode release" 
+weight: 60
+---

content/docs/type-engineering/specification.md

@@ -0,0 +1,19 @@
+---
+title: "Notion de spécification" 
+weight: 10
+---
+
+La notion de spécification correspond à la notion de type en programmation et à
+celle de formule en logique. Il s'agit d'une étiquette, chargée de sens pour
+nous, qui décrit un certain comportement calculatoire, une certaine finalité,
+une certaine attente.
+
+Cette étiquette peut être attachée à un programme pour le décrire (type
+checking) mais on
+pourrait à l'inverse vouloir chercher un programme pour une spécification
+(program synthesis).
+
+Dans la syntaxe transcendantale, il y a deux angles complémentaires pour
+approcher la notion de spécification :
+- le sens d'usine (ou typage ideal)
+- le sens d'usage (ou typage effectif)