BTW: that thing where F* uses Z3 to dissolve boring proofs is definitely worth stealing for Idris.
-
-
Gotta love that syntax of Z3!
1 reply 0 retweets 0 likes -
Replying to @65thdiscord @andreasdotorg and
Wonder whether our in-house constraint solver people would like to have a stab at that...
1 reply 0 retweets 0 likes -
@ozgurakgun and I thought about something like this a while ago... Probably worth doing something some day.1 reply 0 retweets 1 like -
Replying to @edwinbrady @65thdiscord and
I even drafted a fellowship application on the subject! Idris helping our tools, us helping Idris was the crux of idea...
2 replies 0 retweets 1 like -
Replying to @ozgurakgun @edwinbrady and
That kind of thing never seems to be successful. Not shiny enough I guess.
2 replies 0 retweets 0 likes -
Replying to @65thdiscord @ozgurakgun and
eh, there's actually a fair amount of work on this kind of thing, and it's probably where theorem provers are going.
1 reply 0 retweets 0 likes -
Replying to @lenary @ozgurakgun and
I should have been more specific: Any grant application I have been involved in that tried to marry two things to help each other failed.
1 reply 0 retweets 0 likes -
Replying to @65thdiscord @lenary and
I am starting to doubt the "killer application" argument, because I yet have to come across one that convinces the funders & reviewers.
2 replies 0 retweets 0 likes -
Replying to @65thdiscord @ozgurakgun and
The "killer app" is verifying system-level software which can come down to lots of boring bitvector proofs. z3 is very good at bitvectors.
2 replies 0 retweets 0 likes
I definitely want one of those
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.