Various curiosities.

(Thanks to Thierry Martinez for most of these suggestions.)

1 files changed, 32 insertions, 3 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index c9269d5..af96c40 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -117,8 +117,8 @@ Il y a autant de systèmes de typage que de langages de programmation !
 \itempoint Typage \textbf{statique} (à compilation) vs
 \textbf{dynamique} (à exécution) ou mixte.
 
-{\footnotesize En général on préfère : erreur à la compilation $>$
-  erreur à l'exécution $>$ plantage.\par}
+{\footnotesize Mixte = « graduel ».  On préfère : erreur de
+  compilation $>$ erreur à l'exécution $>$ plantage.\par}
 
 \medskip
 
@@ -200,7 +200,8 @@ Somme vide = type inhabité (impossible : aucune valeur).
 \bigskip
 
 \itempoint Types \textbf{fonctions} (= exponentielles).
-P.ex. $\texttt{Nat} \rightarrow \texttt{Bool}$.
+P.ex. $\texttt{Nat} \rightarrow \texttt{Bool}$ (f\textsuperscript{n}
+de $\texttt{Nat}$ vers $\texttt{Bool}$).
 
 \bigskip
 
@@ -468,6 +469,34 @@ linéarité.
 \end{frame}
 %
 \begin{frame}
+\frametitle{Quelques curiosités}
+
+\itempoint En F\#, les unités de mesure sont intégrées au système de
+typage, qui peut donc vérifier l'homogénéité physique.
+
+\bigskip
+
+\itempoint En Rust, le système de typage évite non seulement les
+fuites de mémoire mais aussi certains problèmes de concurrence
+(absence de \textit{race condition} sur les données).
+
+\bigskip
+
+\itempoint Certains langages spécialisés assurent, éventuellement en
+lien avec leur système de typage, des propriétés diverses de leurs
+programmes : terminaison garantie en temps polynomial (Bellantoni \&
+Cook 1992), voire constant (langage Usuba), validation XML (langage
+CDuce), absence de fuite d'information (langage Flow Caml), etc.
+
+\bigskip
+
+\itempoint En Idris, le système de typage est aussi un système de
+preuve (cf. Curry-Howard après) et permet de certifier des invariants
+quelconques d'un programme (p.ex., correction d'un algorithme de tri).
+
+\end{frame}
+%
+\begin{frame}
 \label{typing-and-termination}
 \frametitle{Typage et terminaison}