C++ really has three macro systems: C macros for strcat metaprogramming, C++ templates for constrained hygienic memoized metaprogramming, and overloaded functions for type voodoo metaprogramming arising from the lack of confluence among types and values.
-
-
A couple of weeks ago I did some basics in Coq and Z3. It was neat how Z3 could find contrived instances of function types, but I had the most fun just playing with the Knuth-Bendix FindEquationalProof function in Mathematica.
-
Did an F* tutorial a couple of years ago. Might take another look at it with my current views of trying to "put it all together in a practical language". It's nice they all have browser based REPLs these days.
End of conversation
New conversation -
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.