Finding a billion-user project for Eiffel: How DbC catches the security flaws that Rust misses

[Finnian Reilly]

Finding a billion-user project for Eiffel

How DbC catches the security flaws that Rust misses

Summary of article on eiffel.org

The industry is currently celebrating Rust as a breakthrough in software safety. But Eiffel had a more complete answer to software correctness before Rust's creator was born. This essay argues that the moment has arrived for the Eiffel community to demonstrate that publicly — with a specific project, a real deployment strategy, and a compelling security argument.

https://www.eiffel.org/blog/Finnian%20Reilly/2026/05/finding-billion-user-project-eiffel-how-dbc-catches-security-flaws-rust-misses

[Friedrich Dominicus]

Ich habe DBC für mich in VBA eingebaut, weil es a) funktioniert und b) die Tools für das verbessern der Codebasis mitder Größe der Codebasis nicht klar kommt
DBC  wird imer noch massiv unterschätzt. (Warum auch immer) 

--
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/4e728a1c-4efd-40cf-b397-87f334030a0an%40googlegroups.com.

[lar...@eiffel.com]

Thank you Finnian!

 

From: eiffel...@googlegroups.com <eiffel...@googlegroups.com> On Behalf Of Finnian Reilly
Sent: Friday, May 22, 2026 1:36 PM
To: Eiffel Users <eiffel...@googlegroups.com>
Subject: [eiffel-users] Finding a billion-user project for Eiffel: How DbC catches the security flaws that Rust misses

 

Finding a billion-user project for Eiffel

How DbC catches the security flaws that Rust misses

 

Summary of article on eiffel.org

The industry is currently celebrating Rust as a breakthrough in software safety. But Eiffel had a more complete answer to software correctness before Rust's creator was born. This essay argues that the moment has arrived for the Eiffel community to demonstrate that publicly — with a specific project, a real deployment strategy, and a compelling security argument.

https://www.eiffel.org/blog/Finnian%20Reilly/2026/05/finding-billion-user-project-eiffel-how-dbc-catches-security-flaws-rust-misses

[Ulrich Windl]

Hi!

I have studied the latest Eiffel compiler, nor did I try the latest Rust compiler, but from what I saw in the past was that the Rust compiler was quite good in static analysis during compilation (without the user having to add additional assertions), while Eiffel may detect violated assertions during runtime. So somehow it seems that Rust uses the more advanced compiler technology. However, I'm aware that many errors the Rust compiler complains about cannot happen in Eiffel. This is another performance against comfort issue.
I'd advise the Eiffel community to look at the good things in Rust, rather than bashing at it with a "we are so much better". However, the syntax of Rust is really ugly, maybe even uglier than that of C.

Kind regards,
Ulrich

22.05.2026 13:36:14 Finnian Reilly <frei...@gmail.com>:

> Finding a billion-user project for Eiffel
> How DbC catches the security flaws that Rust misses
>

> *Summary of article on eiffel.org*

> The industry is currently celebrating Rust as a breakthrough in software safety. But Eiffel had a more complete answer to software correctness before Rust's creator was born. This essay argues that the moment has arrived for the Eiffel community to demonstrate that publicly — with a specific project, a real deployment strategy, and a compelling security argument.
> https://www.eiffel.org/blog/Finnian%20Reilly/2026/05/finding-billion-user-project-eiffel-how-dbc-catches-security-flaws-rust-misses

> [Bild][Finding a billion-user project for Eiffel How DbC catches the security flaws that Rust misses.png][cid:7278d4e1-f251-48b9-951e-ee938488cbcd]

>
> --
> 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/4e728a1c-4efd-40cf-b397-87f334030a0an%40googlegroups.com[https://groups.google.com/d/msgid/eiffel-users/4e728a1c-4efd-40cf-b397-87f334030a0an%40googlegroups.com?utm_medium=email&utm_source=footer].

[Finnian Reilly]

On 23/05/2026 15:47, Ulrich Windl wrote:
> I'd advise the Eiffel community to look at the good things in Rust, rather than bashing at it with a "we are so much better". However, the syntax of Rust is really ugly, maybe even uglier than that of C.

Hi Ulrich, the essay isn't bashing Rust — it explicitly acknowledges
what Rust does well. The specific claim is narrower: that Design by
Contract catches logic errors like the sudo-rs CVEs of 2025, which
Rust's static analysis cannot address because they're not memory errors.

--
SmartDevelopersUseUnderScoresInTheirIdentifiersBecause_it_is_much_easier_to_read

[Eric Bezault]

On 23/05/2026 16:47, Ulrich Windl wrote:
> I have studied the latest Eiffel compiler, nor did I try the latest Rust compiler, but from what I saw in the past was that the Rust compiler was quite good in static analysis during compilation (without the user having to add additional assertions), while Eiffel may detect violated assertions during runtime.

What about if Eiffel could detect assertion violations
during compilation? This is the promise of Autoproof.
After many years as a research project, Autoproof is
already able to detect many kinds of assertion violations.
There is a (several year old) prototype/demo available
online:

http://comcom.csail.mit.edu/comcom/#AutoProof

Can you find why class ACCOUNT is broken in this example?
Just fix it and click on Run again...

Having such tool in production would be a killer in
the era of AI generated code. The assertions would be
the specification provided to the AI, and Autoproof
would automatically verify that the generated code
satisfies these assertions.

If there are some companies interested in such technology
and ready to invest money to support this work, this
sponsorship would allow me to join the team and help turn
this research project into a mature production tool
integrated into the Eiffel ecosystem. Please contact me
or Eiffel Software for further discussion.

--
Eric Bezault <er...@gobosoft.com>
Eiffel expert - available for freelance work
https://www.gobosoft.com

[Ian Joyner]

Hello Ulrich.

"I'm aware that many errors the Rust compiler complains about cannot happen in Eiffel. This is another performance against comfort issue.”

I’m not sure about the "performance against comfort issue” point. There are many issues in C-like languages that a compiler must detect, and when not detected are traps the programmer can fall into from mildly irritating to serious and difficult-to-find, only by run-time testing and debugging. That is poor for development performance. Many of these issues just won’t happen in Eiffel. It is not stopping the programmer from expressing anything legitimate, rather just not even being able to express something illegitimate in the first place. That certainly is superior to needing to detect such issues in a compiler or by debugging.

I don’t see that this affects run-time performance in general.

Remember also that Rust is meant for low-level programming. They seem to have forgotten that and now compete in areas that C and C++ should never have been used for, but illegitimately encroached on those areas.

I keep telling people on the net that system and general programming are entirely different. System programming is to define the abstract platform on which other software runs. System programming should take care of lower-level platform details so others don’t have to.

System programming include general programming languages, but with those extras in, which should not be in general languages. Unfortunately, CS students are taught how things work underneath, like memory management, and then think they should deal with these issues. Rust is a language meant to handle those issues.

Where system programmers insist that all should use their system language, they have failed to do their job. Many don’t even understand that is their job.

"I'd advise the Eiffel community to look at the good things in Rust, rather than bashing at it with a "we are so much better”.”

I agree. But we must also be able to express why Eiffel is better. Not exposing system issues is one such place. So actually things that can't happen in Eiffel are someone due to not being able to make system mistakes (because we should not be programming at that level), but there are many non-system traps and issues that aren’t possible in Eiffel.

Sure we should leave the airs-and-graces of superiority to the C/C++ people who consider themselves superior to other programmers. Those other programmers might realise that computing is about computation, not computers.

Ian

To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/2a3ceb58-ba70-41cd-acec-362529266c66%40gmail.com.

[javier...@gmail.com]

I agree that AutoProof is a potential killer app for Eiffel in the era of AI-generated code.

With AutoProof (Code Verifier ), we move bug detection from  `runtime exceptions --> compile-time verification.`

Spec  + DbC  

        -->  LLM generates an implementation to satisfy them  

        --> AutoProof: run static poof (SMT Solvers)  -
        --> Poof Pass?
                Yes --> [Execute] 
                No  --> Violation details back to LLM | Review the Spec  
                   
See a related complementary approach about  formal verification to AI agent workflows https://dl.acm.org/doi/epdf/10.1145/3777544 about 
The article Guardian of Agents is a higher level, for Agents' Orchestrations, a kind of Workflow Verifier.

--Javier