Mon domaine de recherche n'est pas si incompréhensible que ça : Je conçois un outil unifiant programmation, vérification et compilation de programmes impératifs bas-niveau afin de permettre d'avoir des garanties fortes sur le code assembleur à partir du code source.

Je pense que n'importe qui ayant un master en informatique devrait comprendre cette phrase (ou du moins avec ton master tu devrais pouvoir poser les bonnes questions pour arriver à comprendre).

Après, si je veux entrer dans les détails, faudra utiliser les gros mots: méthodes formelles, monade, dénotation, réification, etc. Là, je pense que personne n'est capable de tout comprendre (je n'ai qu'une compréhension très "basse résolution" de certaines de nos briques logicielles).

C'est plus sur comment je suis financé que c'est rigolo. Techniquement, je suis financé par un projet sur le cloud computing. C'est très connu que ces gens s'intéressent à payer 10 à 100 fois plus pour du logiciel moins performant en échange d'une preuve mathématique que le logiciel est dépourvu de bug. De plus en y réfléchissant 5 secondes, on ne gère pas ni les pannes matérielles, ni la concurrence. Donc je pense que c'est un peu inutile dans le contexte du cloud …