From a231bd9587eefba7a4b6c51e3b5339a0320f87c3 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 15 Nov 2023 14:32:48 +0100
Subject: Various curiosities.

(Thanks to Thierry Martinez for most of these suggestions.)
---
 transp-inf110-02-typage.tex | 35 ++++++++++++++++++++++++++++++++---
 1 file changed, 32 insertions(+), 3 deletions(-)

(limited to 'transp-inf110-02-typage.tex')

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
 
@@ -465,6 +466,34 @@ linéarité.
 
 \itempoint Idris : langage fonctionnel + assistant de preuve.
 
+\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}
-- 
cgit v1.2.3