Bon, mon avis va surement être très biaisé, et je suis assez négatif en ce moment, donc ce que je vais t'en dire doit être pris avec des pincettes.
En soit, tout ce qui touche à la logique, à la certification formelle (model-checking, preuves, interprétation abstraite, etc) sont des sujets très intéressant. Maintenant, il faut savoir que ces domaines sont à l'heure actuelle bien plus des sujets de recherche dans les milieux académiques que des choses utilisées dans les entreprises (et ça peut se comprendre). Alors bien sur, dans l'aéronautique, dans le ferroviaire, on utilise des petits morceaux de ces méthodes (bien moins que ce qu'on te vendra en cours par contre). Mais pour ce que j'en ai vu, ça reste très loin de ce qu'on voit dans ce genre de modules, et c'est souvent un peu crade, et loin d'être rempli de beaux objets mathématiques bien définis. Par exemple, l'utilisation des logiques temporelle est très rare, et ils ont souvent tendance à encoder sauvagement de manière ad-hoc les parties temporelles dans une logique moins expressive.
Si tu te spécialise dans le model-checking, et tout ce qui a attrait à la preuve automatique (sur des choses décidables donc), tu pourras trouver quelques domaines d'application, mais si tu vas dans ce domaine pour la beauté des objets mathématiques, sache que ça ne sera pas très "joli". Par contre, tout ce qui est très théorique (théorie des types, assistants de preuves Coq, Agda, etc), qui est mon domaine, ne sont absolument pas utilisés, essentiellement pour des raisons de coût et d'expertise. Petite exception pour la preuve de prog impératifs / évènementiels, car B à réussi à percer un tout petit peu mais ca reste quand même assez anecdotique.
En prime, sache que le domaine de la certification formelle est relativement restreint, et que les salaires n'y sont pas fous par rapport au travail qu'il y a à accomplir.
Enfin, sur le plan humain, j'ai souvent l'impression que les gens qui bossent dedans dans le privé ont les défauts des chercheurs (un peu autistes, souvent incompréhensibles, dans leur monde et tatillon), sans nécessairement en avoir le côté intéressant. Il y a beaucoup d'enculeurs de mouches.
Après, il y a bien entendu pas mal de recherche académique dans ces domaines, avec pas mal de pôles plutôt excellent en France là dedans (j'imagine que tu es en France). Après, il faut bien réfléchir à une carrière dans le public à l'heure actuelle. Ca implique pas mal d'années avec des CDD pourris (post-doc) de 1/2 ans sans garantie d'obtenir un lectureship après....
Le pire selon moi dans les milieux de la preuve formelle dans le public reste le fait que quand tu quitte ces milieux là pour aller faire du dev standard, on te prend un peu de haut parce que tu n'as pas passé des années à écrire du Java ou du C++ (voir pire que tu ne connais pas les derniers langages et outils à la mode). Pas mal de gens sont persuadés que connaitre toutes les dernières libs à la mode est indispensable pour produire du soft. Et quand tu ouvres leur code, tu vois que les concepts les plus basiques, que ça soit de conception, de prog impérative ou OO ne sont absolument pas maitrisé correctement.
En bref, on vit une époque où ça sert pas à grand chose de faire des choses trop compliquées, à part pour se faire plaisir soi même ou pour son égo personnel.Mais n'imagine pas que parce que tu feras des choses compliquées, belles, prouvées et génériques, que tu trouveras facilement du boulot et que tu seras payé correctement. Un développeur web gagnera certainement toujours plus que toi.
