[smaddox]

Verified pre and post conditions would be nice. Especially in the era of LLM's, which can usually fill in the implementation given a sufficiently clear specification.

[082349872349872]

Eiffel is also well over 24 years old (but Albatross is more recent)