diegomrsantos commented on PR #4130:
URL: https://github.com/apache/iggy/pull/4130#issuecomment-5798373884

   @hubcio, agreed. I’ll move the model and supporting files into a separate 
draft PR.
   
   One clarification about CI. `check.py --suite=quick` checks only the Quint 
models, so it can catch model regressions but cannot detect Rust drifting from 
them. A Rust change could leave those checks passing. The current model 
compares failure cases and candidate recovery rules, rather than defining an 
agreed implementation contract. CI would still be useful, with review and Rust 
regressions needed to maintain that connection.
   
   Good catch on `poll_floor`. I’d first reproduce the state transfer case in a 
Rust regression before deciding where the fix belongs.
   
   Yes, I tried Quint Connect a few months ago in a personal project and it 
seemed promising. I checked it again, and public activity looks fairly quiet, 
with the [latest commit in 
May](https://github.com/quint-co/quint-connect/commit/4f018f54fc7dd4cef341d10111427bab59d3b307).
 I’d treat an integration as an experiment for now.
   


-- 
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

To unsubscribe, e-mail: [email protected]

For queries about this service, please contact Infrastructure at:
[email protected]

Reply via email to