LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
240 stars 33 forks source link

Program synthesis with sbv #633

Closed arrowd closed 1 year ago

arrowd commented 1 year ago

Hello, @LeventErkok !

I wrote an SBV-based library that implements a component-based approach for synthesizing straight-line programs: https://github.com/arrowd/sbv-program/ The rendered Haddock documentation is there: http://arrowd.name/sbv-program/

I wonder if it is of any interest of you. Maybe it might be included in the sbv package itself?

LeventErkok commented 1 year ago

Thanks! That looks cool indeed.

SBV is mostly in maintenance mode these days; I'm shying away from putting in any new features unless they are bug-fixes or really simple examples that require almost no maintenance. Your program seems well-deserving of its own hackage package. I'd recommend wrapping it up in a package of its own, putting it on package, and perhaps blogging about it and letting the community know of the cool work you have done.

Cheers!