Dans cet article, nous étudions la compilation modulaire de programmes synchrones impératifs. Nous nous appuyons sur des méthodes formelles pour compiler et valider les applications spécifiées. Nous avons défini et implémenté un langage dédié (LE) et sa sémantique équationnelle qui permet la compilation modulaire des programmes vers différentes cibles logicielles et matérielles (code C, code Vhdl, synthétiseurs fpga, format d'entr\ée d'outils de vérification, ...). Nous montrons que cette sémantique est correcte et nous introduisons un algorithme pour vérifier la causalité qui respecte notre approche modulaire. En nous appuyant sur cette approche formelle, nous avons réalisé une boite à outils pour compiler et vérifier des applications réactives synchrones.