3 ms·

I'm out of context: Was this paper an impactful one? Does it have any ideas that can be applied today?

• Jtsummers 9y ago
  From the paper (brief read) it seems like an attempt at creating one language that could express everything from high level program specifications down to low level implementation details. It seems meant to be paired with a refinement calculus to perform the transformations from one level down to the next. In my understanding some levels are not, strictly, executable by the machine. Though they may be used as ways of verifying their refinements? The modes and objects remind me of more advanced type systems such as Haskell and the MLs, a bit of Ada. The ability to mix high level specs and low level implementation brings to mind design by contract (Eiffel), as well as the methods used in formal specification and verification by Frama C and Spark Ada for systems languages.