3 ms·
> with a naive reference implementation you want to confirm equivalent I'm guessing you know this but in type theories like Agda you can just specify that the
by guerrilla 4y ago
> with a naive reference implementation you want to confirm equivalent
I'm guessing you know this but in type theories like Agda you can just specify that the input and output to an algorithm has the desired properties, rather than needing to specify any reference algorithms. For example, you can just state that an implementation takes a list of X and that it outputs a sorted list of X. Nothing more is necessary in cases like that in such a system, no code, just the single type.
- namibj 4y agoWell, yes, that falls under the second case: behavioral invariants of complex systems. And the reference for "sorting" could likely be a deterministic bogosort and certainly a primitive bubblesort. Even if you're just looking at sorting stability, you're past what your simple "sorted" type would cover. Most things are far less trivial than "sorted list", including (almost?) all interesting practical applications of formal verification in the life of a "normal" software engineer.