[sorincos]

So one builds a model in Reflex based on the requirements, then tests that model. Even when the requirements are complete (which often they are not), the real life implementation afterwards may still bring zillions of problems (my own bugs, using a bad framework, whatever) which this model testing cannot catch... eh.

[BmoreDaniel]

1) The code that users write in Reflex is the code that actually runs. This means that any guarantee about a Reflex program is a guarantee about the real life implementation of that program.

2) Reflex does not use testing to verify a user's code. Instead, Reflex automatically produces fully machine checkable proofs that user-provided code satisfies user-provided specifications. Machine checkable proofs (in a proof assistant) provide the strongest possible guarantee about one's code.