Re: Reason

« les littéraux sont considérés différemment du type ». Veux-tu dire par là que les valeurs, comme 1, et les types, comme int, vivent dans des mondes différents ?

Oui, c'est exactement ça. Et c'est chiant.

Mais une telle situation est présente dans la quasi totalité des langages, à l'exception des langages avec types dépendants (comme Coq).

Oui (je ne connais pas coq), mais cela n’empêche pas d'être très gênant.

Je n'ai jamais dit « pourquoi se faire chier avec un système aussi compliqué »

C'est une figure de style, désolé.

le type des entiers non nuls se définie ainsi en Coq :
Definition non_nul := {n : nat | n <> 0}.

C'est ce que je connaissais des types paramétriques. Le problème est que d’accepter n'importe quoi comme équation booléenne rend la vérification très compliquée. L’intérêt de rester dans des types plus classiques est de simplifier. J'avais lu que la vérification formelle ne marche plus dés qu'il y a des multiplications dans une équation car le nombre des possibles explosent.

Si cela se trouve mon "langage" peut se traduire directement en coq.

Autrement dit on peut mélanger types et littéraux sans problèmes. Est-ce cela que tu veux ?

Oui, même si je voulais juste avoir un langage de description qui m'a l'air bien plus simple que du coq, mais je me trompe peut-être. coq me semble trop complexe pour être utilisé par n'importe qui.

"La première sécurité est la liberté"