Simple Eiffel - Discussions

38 views
Skip to first unread message

Liberty Lover

unread,
Jan 20, 2026, 11:09:49 AM (5 days ago) Jan 20
to Eiffel Users
The discussion(s) board is OPEN for business!!

simple-eiffel · Discussions · GitHub


Ian Joyner

unread,
Jan 20, 2026, 5:18:55 PM (5 days ago) Jan 20
to eiffel...@googlegroups.com
I just wonder if this should be called ’simple’ Eiffel? ’Simple’ has too many connotations. People might overlook you efforts as being dumbed down. I think it is more comprehensive Eiffel.

It seems to have a large scope, so hard to think of correct adjective.

Ian

On 21 Jan 2026, at 03:09, Liberty Lover <rix....@gmail.com> wrote:

The discussion(s) board is OPEN for business!!

simple-eiffel · Discussions · GitHub



--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/7bde2d51-3bec-4292-8bc0-4de7d5c89e1cn%40googlegroups.com.

Liberty Lover

unread,
Jan 20, 2026, 5:24:18 PM (5 days ago) Jan 20
to eiffel...@googlegroups.com
Whelp ... Ian ... I couldn't agree more! It started out with the idea that I want to replace deeply complicated boilerplate Eiffel with simpler API that did in 1-2 lines of code what took 10-30 of repeating boilerplating. But it grew ... and it grew ... and it hasn't STOPPED! LOL  .. and as I write this, you've got me thinking even higher now, now that a very detailed foundation has been established (although growing).

Is there a higher use-case-driven level of library API abstraction that can do 80% of what is needed by programmers, which might (in spirit) return Simple Eiffel to its "simple" roots? Thus, I think you make an excellent point about: Comprehensive Eiffel.

Cheers,

Larry

Liberty Lover

unread,
Jan 20, 2026, 9:06:22 PM (5 days ago) Jan 20
to Eiffel Users
The story from November 11th, 2025 until today is told here:  Simple Eiffel

I am going to finishing exploring Eiffel Loop and wherever that leads and then I think I will take a break for awhile. This has been a very intense 71 days. I need a break!

Bertrand Meyer

unread,
Jan 21, 2026, 5:39:47 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com, me...@inf.ethz.ch

Like Ian I am a bit skeptical about the name as it seems to suggest (from what I see, unwittingly) that either the rest of Eiffel is complicated, or this is a simplified version of Eiffel. But that may be too late to  change and is not the end of the world.

 

More importantly, and possibly off-track since I have not had the time to look at the actual contents, here is a suggestion. If really it is meant to be a better library, it should use model-based contracts, namely MML. That is not so hard to do, and in particular does not require a hard-core competency in formal methods. The idea is simply that you identify a mathematical model behind every Eiffel concept; the model is expressed in terms of simple concepts, typically a set, a sequence, a function, or a combination of two or three of these elements. Then you express the effect of every operation as an operation on these mathematical objects. For example if behind a graphical interface you have a collection of widgets, an operation that removes a widget has a postcondition stating that the associated set does not have that element any more.

 

On MML https://se.inf.ethz.ch/people/schoeller/mml.html, The first reference given there can serve a tutorial on the concepts, but the above comments give the basic idea.

 

A library equipped with contracts of that kind becomes more attractive in my opinion.

 

-- BM

Ulrich Windl

unread,
Jan 21, 2026, 8:35:22 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com
Larry,

you can't do that, because "break" doesn't exist in Eiffel and Ian would never accept it! 😉

Ulrich

Liberty Lover

unread,
Jan 21, 2026, 8:38:11 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com
Dear Bertrand,

Thank you for taking your time to remark on Simple Eiffel and for the thoughtful suggestion regarding model-based contracts.

On the naming: You and Ian are right that "simple" can connote the wrong thing. The name originated from my narrow goal, what was replacing many lines of boilerplate code with far fewer lines through API calls—but the scope has grown considerably over 71 days of development. We now have perhaps 100+ libraries spanning data structures, HTTP, JSON, XML, SQL, cryptography, email, and more (as one can easily surmise). "Comprehensive Eiffel" might be more accurate, though at this point the Simple Eiffel moniker has some momentum. Not the end of the world, as you say, but worth acknowledging.

The outcome of Ian (and now yourself) pointing at naming is why I wrote to Ian that it inspires me to think about another yet higher layer of abstraction on top of and utilizing what has already been built, gathering appropriate simple_* libs together to accomplish higher level jobs that match present 2026 industry needs. Of course, the hope is to simplify (there's that name again) the work of the designer/programmer using Eiffel. The primary thought here would be to isolate those higher API libs into their own "group" (system?) with an entirely new moniker befitting them. And this is where I think a fresh start with MML might prove itself as a great starting block. Nevertheless, backwashing MML on Simple Eiffel libs now is also worthy of a look.

NOTE: The other purpose and semantic frame of "Simple" was for the benefit of 2025/26 American programmers who have their own vernacular. The idea was to use common naming semantics understood in various competitor languages (e.g. Python, Java, Rust, Go, et al) within features of Eiffel classes in Simple Eiffel and even class names themselves. That became even further amplified in the desire to offer multiple names for features to facilitate name semantic frames for particular use cases (e.g. math vs finance vs whatever). All of this is baked into the choice of "Simple". It's a multivectored approach. So, there is that.

Once again—On model-based contracts: This is an excellent suggestion that I'm taking seriously. I've begun researching MML and EiffelBase2 to understand what adoption would entail.

My initial thoughts (Claude helping):

Where MML fits well:
- simple_container (lists, stacks, queues) — natural sequence/set models
- simple_json — JSON objects as maps, arrays as sequences
- simple_xml — tree structures
- simple_graph — relations for edges

Where it's more challenging:
- Many Simple Eiffel libraries use inline C externals for Win32 APIs (per Eric Bezault). Model-based contracts would apply to the Eiffel facade but can't reach into the C layer.
- I/O-heavy libraries (file, process, HTTP client) where effects are external.

Questions I'm investigating:
1. SCOOP compatibility — all Simple Eiffel libraries must work with concurrency=scoop. Does MML work cleanly in that context?
2. What minimal subset of MML is needed? The full library may be more than we require.
3. Tooling — AutoProof would unlock the full verification benefits. What's the current state of tool support?

Planned approach:
1. Create a simple_mml library (or adapt EiffelBase2's MML)
2. Apply model-based contracts to simple_container as a proof of concept
3. Document patterns for wider adoption (albeit possibly muted on existing Simple_*, see above)
4. Evaluate whether this becomes an ecosystem standard

The research you cite—2x more bugs found with strong specifications—is very compelling. Even without formal verification, the discipline of complete postconditions would improve specification quality across the ecosystem. I have started down that road already with the "~\reference_docs\research\06_methodology\AI-slop\prompts\07_maintenance-xtreme", where the AI is pressed into writing both tests and contracts that aim to break the code (uncover bugs, of course). However, this might be the right place to apply MML to the AI's job, which is applied to both existing libraries and new.

FUN FACT: The $ISE_EIFFEL/unstable/library/base2/ has the MML classes. One issue is that the ECF declares <concurrency support="none"/>. But the classes themselves look SCOOP-safe. So, I am faced with doing what I did with Eiffel SQLite, which is to carve off a copy of the MML_* classes, pulling them into a simple_mml and then utilizing them as definitively SCOOP-capable, until such time as ISE Eiffel moves them from unstable to stable. Once that happens, then Claude can certainly and easily adapt the new ISE code.

I'll report back on what we find. If this works well, model-based contracts could become a distinguishing feature of Simple Eiffel libraries.

Best regards,
Larry

Ulrich Windl

unread,
Jan 21, 2026, 9:02:44 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com
Hi!

Maybe use "NT" instead, meaning "new technology", "next technology" or "neural touch" 😉

And an initial thought on MML: Isn't that (having no internal state/commands) creating a lot of garbage (like Java's string addition), causing poor performance?

Ulrich

21.01.2026 11:39:40 Bertrand Meyer <Bertran...@inf.ethz.ch>:

> Like Ian I am a bit skeptical about the name as it seems to suggest (from what I see, unwittingly) that either the rest of Eiffel is complicated, or this is a simplified version of Eiffel. But that may be too late to  change and is not the end of the world.
>  
>
> More importantly, and possibly off-track since I have not had the time to look at the actual contents, here is a suggestion. If really it is meant to be a better library, it should use model-based contracts, namely MML. That is not so hard to do, and in particular does not require a hard-core competency in formal methods. The idea is simply that you identify a mathematical model behind every Eiffel concept; the model is expressed in terms of simple concepts, typically a set, a sequence, a function, or a combination of two or three of these elements. Then you express the effect of every operation as an operation on these mathematical objects. For example if behind a graphical interface you have a collection of widgets, an operation that removes a widget has a postcondition stating that the associated set does not have that element any more.
>  
>
> On MML https://se.inf.ethz.ch/people/schoeller/mml.html, The first reference given there can serve a tutorial on the concepts, but the above comments give the basic idea.
>  
>
> A library equipped with contracts of that kind becomes more attractive in my opinion.
>  
>
> -- BM
>  
>
> *From:* eiffel...@googlegroups.com <eiffel...@googlegroups.com> *On Behalf Of *Ian Joyner
> *Sent:* Tuesday, 20 January, 2026 23:19
> *To:* eiffel...@googlegroups.com
> *Subject:* Re: [eiffel-users] Simple Eiffel - Discussions
>  
>
> I just wonder if this should be called ’simple’ Eiffel? ’Simple’ has too many connotations. People might overlook you efforts as being dumbed down. I think it is more comprehensive Eiffel.
>  
>
> It seems to have a large scope, so hard to think of correct adjective.
>  
>
> Ian
>
> On 21 Jan 2026, at 03:09, Liberty Lover <rix....@gmail.com> wrote:
>  
>
> The discussion(s) board is OPEN for business!!
>
> simple-eiffel · Discussions · GitHub[https://github.com/orgs/simple-eiffel/discussions]
>  
>
>  
>
>  
>
> --
> You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/7bde2d51-3bec-4292-8bc0-4de7d5c89e1cn%40googlegroups.com[https://groups.google.com/d/msgid/eiffel-users/7bde2d51-3bec-4292-8bc0-4de7d5c89e1cn%40googlegroups.com?utm_medium=email&utm_source=footer].
>  
>
> --
> You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/BAFD1734-A84A-4A0C-88F0-745296B62802%40gmail.com[https://groups.google.com/d/msgid/eiffel-users/BAFD1734-A84A-4A0C-88F0-745296B62802%40gmail.com?utm_medium=email&utm_source=footer].
>
> --
> You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/1f2b01dc8ac2%243f86a730%24be93f590%24%40inf.ethz.ch[https://groups.google.com/d/msgid/eiffel-users/1f2b01dc8ac2%243f86a730%24be93f590%24%40inf.ethz.ch?utm_medium=email&utm_source=footer].

Eric Bezault

unread,
Jan 21, 2026, 9:10:57 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com
On 21/01/2026 15:02, Ulrich Windl wrote:
> And an initial thought on MML: Isn't that (having no internal state/commands) creating a lot of garbage (like Java's string addition), causing poor performance?

If MML is only used in assertions, and if it helps Autoproof
statically prove that the assertions will always be satisfied,
then we can safely turn them off at runtime. Hence no
performance penalty. Or did I miss something?

--
Eric Bezault
mailto:er...@gobosoft.com
http://www.gobosoft.com

Liberty Lover

unread,
Jan 21, 2026, 10:24:31 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com

To: Eiffel Users Group

Subject: Progress Report: MML Integration and Contract Refinement

This and other recent threads have been incredibly productive. I would like to report on concrete progress following Bertrand's suggestions and Eric’s detailed critique regarding the use of the Mathematical Model Library (MML) and automated reasoning.

1. Creation of the simple_mml Library

Following Bertrand's recommendation, we extracted the MML classes from $ISE_EIFFEL/unstable/library/base2/mml/ to create a Void-safe and SCOOP-compatible simple_mml library. This library provides:

  • MML_MODEL: Base class with model equality operator |=|.

  • MML_SEQUENCE [G]: Ordered collections (stacks, queues, lists).

  • MML_SET [G]: Unique unordered elements.

  • MML_BAG [G]: Collections with counted duplicates.

  • MML_MAP [K, V]: Key-value pairs.

  • MML_RELATION [K, V]: Multi-valued keys.

  • MML_INTERVAL: Integer ranges.

Technical Note: Void Safety and MML

The simple_mml library is now fully void-safe (void_safety="all") and SCOOP-compatible (concurrency="scoop"). All 26 tests pass.

The primary challenge was the model_equals feature in MML_MODEL:

Code snippet
frozen model_equals (v1, v2: detachable ANY): BOOLEAN

With unconstrained generics ([G]), the compiler raises VUAR(2) errors when passing generic type parameters to detachable ANY arguments.

Our initial attempt used [G -> ANY] constraints, but this was incorrect as it constrains G to attached types only. The correct solution is [G -> detachable ANY]:

Code snippet
class MML_SET [G -> detachable ANY]
class MML_SEQUENCE [G -> detachable ANY]
class MML_BAG [G -> detachable ANY]
class MML_MAP [K -> detachable ANY, V -> detachable ANY]
class MML_RELATION [G -> detachable ANY, H -> detachable ANY]

This declared constraint allows the generic parameter to be either attached or detachable, ensuring compatibility with model_equals. Lesson learned (soon to be forgotten by Claude): When working with void-safe generics, the constraint must match the detachability of the target parameter type, not just the base type.


2. Methodology Integration

We have updated our AI workflow prompts (steps 01–07) to incorporate MML from the earliest specification phases:

  • Step 02 (Define Structure): Inclusion of model query signatures.

  • Step 04 (Write Postconditions): Preference for model-based postconditions (e.g., model |=| old model & x).

  • Step 05 (Write Invariants): Establishing model consistency.

  • Step 07 (Xtreme Maintenance): Implementing "Contract Assaults" to stress-test specifications.


3. Improvements to simple_sorter

We addressed Eric’s specific criticisms of the previous implementation:

IssueResolution
Missing sorted postconditionAdded result_sorted: is_sorted (a_array, a_key, a_descending).
Missing contracts in descendantsAdded full pre/postconditions to heap_sort, merge_sort, etc.
Naming inconsistenciesRenamed to create_array_from_list (query) and copy_array_to_list (command).
Arbitrary is_empty pre-conditionRemoved; empty containers are now treated as trivially sorted.
Multi-key sortingAdded sort_by_then_by and sort_by_comparator with agent support.
Redundant /= Void checksRemoved; unnecessary in a void-safe system.

The Role of AutoProof

I am going to assume that Eric is correct regarding the performance trade-offs of complex assertions. We encountered this directly with an $O(n^2)$ is_permutation postcondition that hung during a 100K-element adversarial test:

Code snippet
ensure
    count_unchanged: a_array.count = old a_array.count
    result_sorted: is_sorted (a_array, a_key, a_descending)
    -- result_permutation: is_permutation (a_array, old a_array.twin)
    -- Note: Disabled for runtime performance; requires static verification.

With AutoProof, these expensive postconditions could be verified statically once, then safely disabled for production. This validates the MML + AutoProof synergy Bertrand and Eric described.


Perspective on the Wider Context

This discussion highlights the unique rigor of the Eiffel ecosystem. In mainstream stacks—Java, Python, Rust, or Go—developers often lack both the vocabulary and tools for this conversation. They cannot write ensure result_sorted as a native language feature; they rely on "testing by example" rather than "specification by contract."

While Claude’s initial simple_sorter was flawed within our Eiffel context and group expertise, its output still included void-safe types and feature categorization—foundations other languages cannot replicate. Our ability to fix AI-generated code through systematic methodology is a testament to Eiffel’s 40-year investment in software engineering.

Next Steps

  1. Apply simple_mml to simple_container as the next proof-of-concept.

  2. Investigate AutoProof tooling for static verification of expensive postconditions.

  3. Document MML patterns for broader ecosystem adoption.

Thank you for the constructive feedback. This is exactly how we push the state of the art forward.

Best regards,

Larry


Liberty Lover

unread,
Jan 21, 2026, 10:35:54 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com

Eric Bezault

unread,
Jan 21, 2026, 10:42:45 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com
On 21/01/2026 16:24, Liberty Lover wrote:
> The primary challenge was the |model_equals| feature in |MML_MODEL|:
>
> Code snippet
>
> |frozen model_equals (v1, v2: detachable ANY): BOOLEAN|
>
> With unconstrained generics (|[G]|), the compiler raises *VUAR(2)*
> errors when passing generic type parameters to |detachable ANY| arguments.
>
> Our initial attempt used |[G -> ANY]| constraints, but this was
> incorrect as it constrains |G| to /attached/ types only. The correct
> solution is *|[G -> detachable ANY]|*:

That is not the correct solution. An unconstrained formal generic
parameter `[G]` is equivlent to `[G -> detachable separate ANY]`.
So what you did was not to add `detachable` but rather to
remove `separate`. This makes it less SCOOP-friendly.

The correct solution is rather to change the signature of
`model_equals` to:

frozen model_equals (v1, v2: detachable separate ANY): BOOLEAN

Liberty Lover

unread,
Jan 21, 2026, 11:03:06 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com
Eric,

This is where I trust you far more than Claude. I asked Claude to research to find evidence that detachable separate is correct. This is what it came up with:

  What I Found

  The eiffel.org documentation explicitly states:
  "unconstrained genericity, as in LIST [G], may be viewed as an abbreviation for genericity constrained by ANY, as in LIST [G ->
  ANY]"
  — https://www.eiffel.org/doc/eiffel/I2E-_Combining_Genericity_and_Inheritance

  Regarding separate:
  "The keyword separate is not part of the Eiffel standard. It has been introduced in ISE Eiffel to support the SCOOP mechanism."
  — https://www.gobosoft.com/eiffel/syntax/

  The search results reference a York University page (seldoc.eecs.yorku.ca) that reportedly stated FOO [G] = FOO [G → detachable
  separate ANY], but that site is currently inaccessible and I cannot verify it.

  My Assessment

  The claim that [G] implicitly includes separate appears to be either:
  1. An ISE EiffelStudio implementation detail (not in the ECMA standard)
  2. A logical inference about what SCOOP-safe code would require
  3. Potentially outdated or incorrect information

  You're right to ask for evidence. I should not have stated Eric's claim as fact without verification. The authoritative Eiffel
  documentation I found only says [G] = [G -> ANY], with no mention of detachable or separate being implicit.

  Would you like me to ask Eric directly for his source, or should we proceed with the understanding that the [G -> detachable ANY]
  constraint we used is the correct approach for void-safe code that needs to pass values to detachable ANY parameters?

Again, I trust you far more than Claude in all cases. So, the question becomes: What's the source of your response? Is it time to update the ECMA standard to reflect SCOOP? (I don't recall if the standard included Void-safety or not)

Larry

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.

Liberty Lover

unread,
Jan 21, 2026, 11:13:19 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com

Summary of Results

LibraryConstraintCompilationTests
simple_mml
[G -> detachable separate ANY]
Success26/26 pass
simple_container
[G -> detachable separate ANY]
Success51/51 pass

Both libraries compile successfully, and all 77 tests pass with the explicit separate keyword.


Eric,

Thank you for the clarification on generic constraints. We tested your observation that [G] is equivalent to [G -> detachable separate ANY] and that using [G -> detachable ANY] actually removes the implicit separate.

Based on your feedback, we updated both simple_mml and simple_container to use the explicit [G -> detachable separate ANY] constraint.

Changes Implemented:

  1. Updated MML_MODEL: Modified model_equals to:

  1. frozen model_equals (v1, v2: detachable separate ANY): BOOLEAN

  1. Updated simple_mml: Applied [G -> detachable separate ANY] to all generic classes (MML_SET, MML_SEQUENCE, MML_BAG, MML_MAP, MML_RELATION).

  2. Updated simple_container: Applied the same constraint across all 11 generic classes.

Results:

  • simple_mml: Compiles, 26 tests pass.

  • simple_container: Compiles, 51 tests pass.

The explicit separate constraint works correctly and maintains SCOOP compatibility while still allowing the generic parameters to be passed to model_equals for void-safe model equality comparisons.

Follow-up Question:

Already stated, but once more could you point me to official documentation that confirms [G] = [G -> detachable separate ANY]? I searched eiffel.org and the ECMA-367 standard but only found references stating [G] = [G -> ANY], without mention of detachable or separate.

Is this an ISE EiffelStudio-specific behavior since separate is not part of the core ECMA standard?

Thanks,

Larry


--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.

Eric Bezault

unread,
Jan 21, 2026, 11:24:32 AM (4 days ago) Jan 21
to eiffel...@googlegroups.com
On 21/01/2026 17:02, Liberty Lover wrote:
> Again, I trust you far more than Claude in all cases. So, the question
> becomes: What's the source of your response?

Since we don't have SCOOP documented in the standard yet,
I'm just using my **human** intelligence as source. Just
think at little bit: an unconstrained formal generic
parameter means that there is **no** constraint. So if we
have:

class LIST [G]

I should be able to write:

my_list: LIST [separate FOO]

or:

my_list: LIST [detachable FOO]

or:

my_list: LIST [detachable separate FOO]

There is only one way to allow that: we have
to assume that:

class LIST [G]

is equivalent to:

class LIST [G -> detachable separate ANY]

and not just:

class LIST [G -> ANY]

It's as simple as that. It's pure logic, even if it's
not explicitly documents in the standard yet.

Liberty Lover

unread,
Jan 21, 2026, 12:38:04 PM (4 days ago) Jan 21
to eiffel...@googlegroups.com
That works for me. Confirmed at least from the context that the Eiffel compiler doesn't gripe about it. 

Still -- it would be nice to have the ECMA standard updated to 2026.


--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.

Liberty Lover

unread,
Jan 21, 2026, 1:14:19 PM (4 days ago) Jan 21
to eiffel...@googlegroups.com

simple_mml Ecosystem Integration Report

Overview

Over the past few hours, I have instructed Claude to apply the simple_mml (Mathematical Modeling Library) to 25 libraries in the simple_* Eiffel ecosystem. We utilized a systematic methodology termed "X03 Contract Assault" to strengthen specifications and verify consistency.

Scope and Metrics

MetricValue
Libraries integrated25
Source files modified49
Total tests passing750+
Bugs discovered2
Redundant preconditions removed110+

MML Type Distribution

MML TypeLibraries UsingPrimary Use Case
MML_SEQUENCE19Ordered collections, lists, arrays
MML_MAP13Key-value stores, indexes, registries
MML_SET11Unique collections, domains, keys
MML_BAG1Multisets (sorting permutation proofs)
MML_RELATION1Graph edges
MML_INTERVAL1Date/time ranges

Integrated Libraries: simple_cache, simple_config, simple_container, simple_csv, simple_datetime, simple_diff, simple_encoding, simple_factory, simple_file, simple_graph, simple_hash, simple_http, simple_json, simple_logger, simple_math, simple_mock, simple_persist, simple_process, simple_regex, simple_scheduler, simple_sorter, simple_sql, simple_testing, simple_validation, simple_xml.


Key Findings

1. Model Queries Enable Precise Specifications

Using model queries allows us to prove properties that were previously difficult to express. For example, in simple_sorter, we can now mathematically prove a sort is a permutation:

Code snippet
sort (a_array: ARRAY [G]; a_key: FUNCTION [G, COMPARABLE]; a_descending: BOOLEAN)
    ensure
        model_sorted: is_sequence_sorted (array_to_sequence (a_array), a_key, a_descending)
        model_permutation: array_to_bag (a_array) |=| old array_to_bag (a_array.twin)

2. SCOOP Compatibility

Following Eric Bezault's clarification, all MML classes now utilize the most permissive constraint to ensure full SCOOP and Void Safety compatibility:

  • class MML_SET [G -> detachable separate ANY]

  • class MML_MAP [K -> detachable separate ANY, V -> detachable separate ANY]

3. Void-Safety Audit

The transition to attached types by default allowed us to strip a significant amount of "defensive" code that is no longer reachable:

  • simple_regex: 55+ redundant preconditions removed.

  • simple_hash: 23 redundant preconditions removed.

  • simple_xml: 19 redundant preconditions removed.

4. Bugs Discovered

The rigor of model-based postconditions exposed two latent bugs:

  • simple_cache: LRU eviction failed for duplicate keys because it used prune_all (object equality) instead of same_string for STRING keys.

  • simple_mock: A VAPE error was caught where HTTP status constants used in preconditions were incorrectly exported to {NONE}.


Impact on Contract Quality

The shift from implementation-based contracts to mathematical modeling significantly elevates the reliability of the code:

  • Before MML (Implementation-coupled):

    ensure count_updated: entries.count = old entries.count + 1

  • After MML (Abstract Property):

    ensure key_in_model: model_entries.domain [a_key]

    ensure key_is_most_recent: model_keys.last.same_string (a_key)

Conclusion

simple_mml demonstrates that lightweight mathematical modeling is practical for real-world Eiffel development. The six core MML classes successfully covered the modeling needs of 25 diverse libraries. This integration validates Design by Contract at scale: 750+ tests pass with strengthened specifications, and two subtle bugs were identified and fixed.

Best regards,

Larry


On Wed, Jan 21, 2026 at 5:39 AM Bertrand Meyer <Bertran...@inf.ethz.ch> wrote:

Ulrich Windl

unread,
Jan 21, 2026, 1:34:28 PM (4 days ago) Jan 21
to eiffel...@googlegroups.com
Unfortunately "old-time Eiffelists" would consider that below as unconstrained. To me it looks odd when adding additional keywords actually _removes_ restrictions (as it seems to me).

Ulrich

21.01.2026 17:24:27 Eric Bezault <er...@gobosoft.com>:

Eric Bezault

unread,
Jan 21, 2026, 2:29:11 PM (4 days ago) Jan 21
to eiffel...@googlegroups.com
On 21/01/2026 19:14, Liberty Lover wrote:
> 2. SCOOP Compatibility
>
> Following Eric Bezault's clarification, all MML classes now utilize the
> most permissive constraint to ensure full SCOOP and Void Safety
> compatibility:
>
> *
>
> |class MML_SET [G -> detachable separate ANY]|
>
> *
>
> |class MML_MAP [K -> detachable separate ANY, V -> detachable
> separate ANY]|

Just to make things clear, there is no need to make
these generic constraints explicit. These are the
default.

Liberty Lover

unread,
Jan 21, 2026, 3:47:51 PM (4 days ago) Jan 21
to eiffel...@googlegroups.com
I don't think detachable is the default because an MML_* [G] doesn't compile. However, an MML_* [G -> detachable ANY] or MML_* [G -> detachable separate ANY] does compile. The question remains (beyond just reasoned logic), what is the specification? And here I think someone with ISE Eiffel should chime in with the answer and whether we're ever going to get a 2026 update to the ECMA standard.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.

Eric Bezault

unread,
Jan 21, 2026, 4:11:29 PM (4 days ago) Jan 21
to eiffel...@googlegroups.com
On 21/01/2026 21:47, Liberty Lover wrote:
> I don't think detachable is the default because an MML_* [G] doesn't
> compile. However, an MML_* [G -> detachable ANY] or MML_* [G ->
> detachable separate ANY] does compile.

What error do you get?

> The question remains (beyond just
> reasoned logic), what is the specification? And here I think someone
> with ISE Eiffel should chime in with the answer and whether we're ever
> going to get a 2026 update to the ECMA standard.

This is what we have in the unpublished version of the standard
which is still being worked on:

~~~~
Definition: Constraint, constraining types of a Formal_generic

The constraint of a formal generic parameter is its `Constraint` part if
present, and otherwise `–> separate detachable ANY`.
~~~~

Liberty Lover

unread,
Jan 21, 2026, 4:32:17 PM (4 days ago) Jan 21
to eiffel...@googlegroups.com

Eric,

The recent errors were not compile-time, but contract violations caught by the new MML-based postconditions. Here is the breakdown of what we encountered:

1. simple_regex (2 failures)

  • Failed Tests: test_match_all_basic, test_match_all_as_strings

  • The Postcondition: 

    ensure
       result_model: Result.matches_model |=| old Result.matches_model.extended (...)

  • The Cause: The MML |=| operator performs a deep equality check calling is_equal on elements. Because SIMPLE_REGEX_MATCH had not overridden is_equal, it defaulted to reference equality. When the old expression created a deep_twin copy of the model, the copied match objects had different references than the new result objects.

  • Resolution: Overriding is_equal in SIMPLE_REGEX_MATCH to compare values rather than references resolved the failure.

2. simple_process (7 failures)

  • Failed Tests: test_output_of_command, test_output_of_command_echo, test_output_of_command_dir, etc.

  • The Postcondition:

    Code snippet
    ensure
        execution_recorded: execution_count = old execution_count + 1
    
  • The Cause: This was a genuine logic omission exposed by the contract. The output_of_command feature calls execute, which delegates to execute_in_directory. However, execute_in_directory was failing to increment the internal execution_count_impl.

  • Resolution: Added the missing increment to the implementation, ensuring the abstract count correctly mirrors the internal execution state.

I didn't do a deep dive into the precise nature of the issue except that Claude kept trying to change [G] into [G -> ANY] with the idea that this would resolve the issue (as yet not totally defined to me in particular). Nevertheless, I complained back to Claude that the two were identical as the ANY constraint is implied. When I made that comment then it stop flailing away at the code back-and-forth with that solution. It was something you wrote that finally triggered me to suggest to Claude that making the Generic constraint detachable would stop the flailing, which it did. With that in place, Claude focused on what is talked about above — broken postcondition contracts. You then brought up the idea of adding the separate keyword to the Generic constraint, which did not necessarily change anything with regard to the compile or to the previously-but-now-working postcondition contracts. Thus, I have left the matter alone. Without specifications to guide beyond logical surmising, I think the matter can be laid to rest. What do you think?

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.

Eric Bezault

unread,
Jan 21, 2026, 4:45:21 PM (4 days ago) Jan 21
to eiffel...@googlegroups.com
On 21/01/2026 22:32, Liberty Lover wrote:
> The recent errors were not compile-time, but contract violations caught
> by the new MML-based postconditions. Here is the breakdown of what we
> encountered:

I don't see how this is related to whether the default constraint
`-> detachable separate ANY` is made explicit or not.

What I'm interested in is to have tests which are working, and
then just remove the constraint `-> detachable separate ANY`
and no other modifications.

I'm sorry to insist, but `-> detachable separate ANY` is the
default constraint.

Liberty Lover

unread,
Jan 21, 2026, 5:15:29 PM (4 days ago) Jan 21
to eiffel...@googlegroups.com
  Eric,

  You were right. I apologize for the confusion.

  I ran a clean experiment as you suggested:

  1. Started with working tests (simple_mml: 26 tests pass)
  2. Removed -> detachable separate ANY from ALL MML generic classes:
    - MML_SET [G]
    - MML_BAG [G]
    - MML_SEQUENCE [G]
    - MML_MAP [K, V]
    - MML_RELATION [G, H]
  3. Recompiled simple_mml: compiles, 26 tests pass
  4. Recompiled consumers (simple_container, simple_sorter, simple_regex): all compile, 216 additional tests pass

  Result: Zero compile errors. Zero test failures.

  The explicit constraint was purely redundant, exactly as you said. I've committed the simplified declarations.

  The issues I was experiencing earlier (test failures, contract violations) were unrelated to generic constraints - they were bugs
  in my code (missing is_equal overrides, missing model state updates). I incorrectly attributed them to the constraint syntax.

  Thank you for pushing back and insisting on a proper experiment.

  Claude
----

My take — Claude was flailing back and forth between [G] and [G -> ANY] as though doing that would solve an issue is was finding with compiling. It now makes me wonder if it was fighting its own stupid choices. Let me clue you in:

I have noticed that for some unknown-to-me reason, it chooses to compile outside of the project space, where I end up with EIFGENs in my Simple Eiffel root folder (e.g. locally that is d:\prod\*). I end up with not only an stray EIFGENs but stray simple_*.rc files and an exception_trace.log file. This appears to be symptomatic of Claude:

1. Forgetting — new sessions or session compaction causes the AI to lose memory of past learning. Therefore, until AI's (in general) can have long-term memory, their operation should be treated with a high degree of suspicion. We should NEVER allow ourselves to treat an AI as though it "remembers." It doesn't.

2. Hallucination — while the matter of creating and generating compile artifacts (e.g. like EIFGENs) beyond the core project folder seems to work in Claudes world, doing so may have unintended consequences. I don't know how to deal with those, make Claude stop, or otherwise diagnose the issue to know where it hurts rather than helps.

So, when I say that Claude's EIFGENs may have become somehow corrupt, I am leaning in on this scenario as a possible source of the earlier compile issue that was causing the AI to bounce back-and-forth with a hallucinated issue, hallucinated diagnosis, and hallucinated solution. A human would have seen this. Thankfully, folks here like yourself who are outside of the AI + Me local context could cast some sunlight on the issue to help break the cycle.

In fact, here is a screen shot of my system right now. These are as I have described above. I will delete these now, but ultimately Claude makes some stupid choice that causes it to do this all over again. I have found no way to make it stop.

image.png

And here is the interior of the stray EIFGENs:

image.png

Take note of the datetime on those folders. It's all today.


--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.

Liberty Lover

unread,
Jan 21, 2026, 5:24:12 PM (4 days ago) Jan 21
to eiffel...@googlegroups.com
Leaves me with cleanup

image.png
Reply all
Reply to author
Forward
0 new messages