Selon Tanenbaum c'est l'approche la plus révolutionnaire de toute...et c'est Microsoft Research qui poursuit ce but ! C'est un nouveau type d'OS, nommé Singularity, et il est basé sur un language formel spécifique (Sing#) qui permet, par design, une sécurité absolue.
J'ai été voir (pas très profondement) sur le site et Sing# c'est de la programmation par contrat (ou alors j'ai loupé des bouts) mais ce n'est pas suffisant par assurer une sécurité absolue. C'est la même chose que pour eiffel ou tout ce qui a suivi, en fait c'est une méthode semi-formelle et comme on ne fait pas de preuves de corrections on n'a pas de sécurité absolue. Enfin rien n'empèche de faire les preuves a postériori mais les approches de certifications de programmes qui collent trop au code sont très difficiles à mener a terme.
C'est marrant cela ressemble énormément à isaac (contrat+objet).
# Contrat
Posté par Joris R (site web personnel, Mastodon) . En réponse au journal La vengeance de Tanenbaum. Évalué à 5.
J'ai été voir (pas très profondement) sur le site et Sing# c'est de la programmation par contrat (ou alors j'ai loupé des bouts) mais ce n'est pas suffisant par assurer une sécurité absolue. C'est la même chose que pour eiffel ou tout ce qui a suivi, en fait c'est une méthode semi-formelle et comme on ne fait pas de preuves de corrections on n'a pas de sécurité absolue. Enfin rien n'empèche de faire les preuves a postériori mais les approches de certifications de programmes qui collent trop au code sont très difficiles à mener a terme.
C'est marrant cela ressemble énormément à isaac (contrat+objet).