Hacker News new | ask | show | jobs
by Trung0246 23 days ago
How does this differ from https://github.com/verus-lang/verus
1 comments
isubasinghe 23 days ago
Creusot works on functionalisation if I recall correctly. It translates to coma (https://coma.paulpatault.fr/language/program.html).

Verus encodes directly to SMT.

Creusot may gain some more automation perhaps from this approach.

link