3 ms·
Think of writing a TLA+ spec as structured thinking with error checking. It helps create a correct algorithm. Having your code implement the algorirthm correctl
by dmos62 6y ago
Think of writing a TLA+ spec as structured thinking with error checking. It helps create a correct algorithm. Having your code implement the algorirthm correctly is a different problem.
There was a Racket language that actually syntesized programs from specs (e.g. go from spec of a sorting algo to its implementation automatically), but I forget what it's called. Fun to play around with.
- Jtsummers 6y agoI've seen a couple things on using Racket for code synthesis. My google search revealed Rosette, which wasn't what I was thinking of. The other work may have been in Scheme, using minikanren, but my Google Fu seems weak this morning. https://docs.racket-lang.org/rosette-guide/index.html https://docs.racket-lang.org/rosette-guide/index.html
- hwayne 6y agoFun fact: Emina Torlak also wrote Kodkod, the constraint solver used to convert Alloy specs into SAT problems. She's pretty cool!