Formal Methods: Whence and Whither, Jonathan Bowen

 https://www.bcs.org/events-calendar/2025/december/hybrid-facs-agm-and-peter-landin-semantics-seminar

Title: Formal Methods: Whence and Whither

Abstract: Alan Turing arguably wrote the first paper on formal methods over 75 years ago.Since then, there have been claims and counterclaims about formal methods. Tool development has been slow but aided by Moore’s Law with the increasing power of computers. Although formal methods are not widespread in practical usage at a heavyweight level, their influence has crept into software engineering practice to the extent that they are no longer necessarily called formal methods in their use. In addition, in areas where safety and security are important, with the increasing use of computers in such applications, formal methods are a viable way to improve the reliability of such software-based systems. Their use in hardware, where a mistake can be very costly, is also important. This talk explores the journey of formal methods to the present day and speculates on future directions, including the use of Artificial Intelligence.

 

Jonathan cite Théophile Gautier, voici le poème complet :

Oui, l'œuvre sort plus belle
D'une forme au travail
Rebelle,
Vers, marbre, onyx, émail.

Point de contraintes fausses !
Mais que pour marcher droit
Tu chausses,
Muse, un cothurne étroit.

Fi du rhythme (1) commode,
Comme un soulier trop grand,
Du mode
Que tout pied quitte et prend !

Statuaire, repousse
L'argile que pétrit
Le pouce
Quand flotte ailleurs l'esprit :

Lutte avec le carrare,
Avec le paros dur
Et rare,
Gardiens du contour pur ;

Emprunte à Syracuse
Son bronze où fermement
S'accuse
Le trait fier et charmant ;

D'une main délicate
Poursuis dans un filon
D'agate
Le profil d'Apollon.

Peintre, fuis l'aquarelle,
Et fixe la couleur
Trop frêle
Au four de l'émailleur.

Fais les sirènes bleues,
Tordant de cent façons
Leurs queues,
Les monstres des blasons ;

Dans son nimbe trilobe
La Vierge et son Jésus,
Le globe
Avec la croix dessus.

Tout passe. - L'art robuste
Seul a l'éternité.
Le buste
Survit à la cité.

Et la médaille austère
Que trouve un laboureur
Sous terre
Révèle un empereur.

Les dieux eux-mêmes meurent,
Mais les vers souverains
Demeurent
Plus forts que les airains.

Sculpte, lime, cisèle ;
Que ton rêve flottant
Se scelle
Dans le bloc résistant !
 
 
Théophile Gautier, Émaux et camées, 1852.
Texte intégral dans Gallica : Paris, Charpentier, 1872 

 https://en.wikipedia.org/wiki/Th%C3%A9ophile_Gautier

 

(1) je découvre cette orthographe (qu'on dit "désuète), je ne connaissais que "rythme".

Comments

Post a Comment

Popular posts from this blog

Ce que je dois à Jean-Raymond Abrial

Image
 Quand ai-je découvert Jean-Raymond Abrial ?  Peut-être bien que c'est quand j'ai fait acheter les actes de la conférence de Cargèse et que j'ai lu son article Data Semantics . Ou est-ce lors de la lecture des publications de la DER-IMA d'EDF (située à Clamart) ? Ce qui est sûr c'est que j'ai découvert Z dans le Meyer Baudoin, Méthodes de Programmation chez Eyrolles, puis dans le Delobel Adiba, Bases de données chez Dunod. Quand j'ai débuté en "informatique de gestion" (en I.U.T "Informatique") je trouvais que ce que je lisais était bien peu "scientifique". "Information" "donnée" "rubrique" etc.  Pour "donnée" j'ai appris les théorèmes de Jean-Louis Rigal qui était prof à l'Université Dauphine. Facile : Th1, "Une donnée n'est pas donnée" car c'est le résultat d'une abstraction, Th 2. "Une donnée n'est pas donnée" car une fois donnée, ce n'est...
Read more

Jean-Raymond Abrial (1938, 2025)

Image
  Jean-Raymond Abrial (1938, 2025) Jean-Raymond Abrial est décédé les 26 mai 2025 la vieille de la conférence qui a eu lieu dans le cadre des Journées Scientifiques de l'université de Nantes et qui traitait de ses travaux et de leur mise en oeuvre dans différentes domaines.J.-R Abrial est né en 1938 à Versailles. Après des études au Prytanée militaire de la Flèche, il fera l'Ecole Polytechnique. En 1960 il sera ingénieur du génie maritime. Il sera boursier du gouvernement français à Stanford University puis au Centre de Programmation de la Marine où il travaillera sur une version du langage LTR (Langage Temps Réel). C'est là que Gérard Le Lann, qui a fait partie de l'équipe ayant conçu Internet, l'a connu. J.-R Abrial est pour lui "l'un des plus grands informaticiens français ! Peu enclin à épouser les « modes » qui agitent plus ou moins régulièrement les communautés scientifiques. Liberté de penser, de créer, et liberté d'essaimer !".A Grenoble, d...
Read more

On B, Jean-Raymond Abrial

 Cet article date du temps où Jean-Raymond Abrial habitait rue des plantes à Paris. Digilog était deveni Steria, mais pas encore Clearsy. Donc d'avant 2001. On B Jean-Raymond Abrial Consultant, 26, rue des Plantes, 75014, Paris. abrial@steria.fr In  the B-Book [Abr96], an introduction entitled “What is B ?” presents it in a few pages. There is no point in reproducing this introduction here. There is, however, clearly a need to have in this book a sort of informal presentation of B complementing that of the B-Book for those readers who are not familiar with this approach. This is the purpose of this short text, where the emphasis will be put on the question of the development process with B. At the end of the text, I will also cover some more general problems concerning B (tool, education, research, future). B is o “Debugger”. The aim of B is very practical. Its ambition is to provide to industr...
Read more