Theorem Provers Are Refactoring Tools
HTML-код
- Опубликовано: 16 сен 2024
- Craft vs Cruft: Meditations on software quality. Episode 56: Theorem Provers Are Refactoring Tools
Follow Ray Myers:
LinkedIn: / cadrlife
Twitter: / lambdapocalypse
Empathy In Tech podcast: empathyintech.com
Mender.AI
References:
Source code:
github.com/ray...
Gilded Rose kata, Emily Bache Repo
github.com/emi...
ACL2
www.cs.utexas....
Comby
comby.dev/
Simplify-Defun
www.cs.utexas....
Kestral
www.kestrel.ed...
Proofpad (ACL2 in browser)
new.proofpad.org/
I love how you stumbled upon this... It makes total sense given the normalization / reduction steps taking place...
Absolutely, it's one of those moments when you realize you've learned the same concept twice for different reasons, it opens up possibilities.
I think compiler passes are another example of this concept, semantics-preserving tree transformations. So some of the work on certified compilers should be applicable to refactoring
Excellent!
Wow! What if Ray solves refactoring? If teams could run an auto-refactoring tool that executes a bunch of reasonable refactoring rules in the same way they currently run their auto-formatting tool, it sort of changes everything.
Ray-Factor does have a ring to it :) I see refactoring as something where the target depends on your current goals, so I don't know if it'll ever be quite as fire-and-forget as formatting/linting. But these kinds of workflows - express one intention and 30 steps unfold - I think that's very possible.
A major limiting factor is that our mainstream languages are not verification-friendly, so we either climb that analysis mountain or write more code in provable languages. Purely-functional languages might have a new secret weapon.
I found this interesting, but am a little disappointed that the issue of choosing what rules to apply during the refactoring ended up being solved by using an existing library without (me) understanding the underlying process fully.
You kind of gloss over your own knowledge there, I have no idea how you confidently defined the list of manual refactoring steps (14:23) and would love to see a video about it from your POV, be it methodology or just raw experience.
Regardless, I'm glad I stumbled across your video and hope to see more of your videos in the future :)
Thanks @Maedas, this is very helpful feedback! I've been making some more advanced content this year and I'm not always very good abount saying what knowledge it depends on. I'll try and improve that going forward.
I'm linking my playlist of refactoring videos and the older ones are more focused on my thought process as it occurs rather than these new techniques for tool support.
Better yet, some teacher's that I look up to on this are Arlo Beshee (e.g. "Mastering Legacy Code Incrementally" talk) and Emily Bache (channel @EmilyBache-tech-coach). Cheers!
ruclips.net/p/PLRe4i06eNAcDY4XjMfyEMK6hjnoIOpqk2
Oh, and the specific list of rules you're asking about were the same ones that I wrote in the Comby UI while inspecting the code in 9:45 - 13:00, if that helps at all.
Mostly Boolean Logic simplification - might be a good topic for a followup video.
@@craftvscruft8060 Yeah the list is no problem, I saw and understood what you did I just have no idea how you came to the choices you did while doing it; If I had to build something like that it would take me 30 min and I would be very unsure about my methodology, kind of just guessing/looking at articles/asking around.
A follow up on Boolean Logic simplification sounds lovely
@@craftvscruft8060 thank you for taking my feedback correctly, I don't mean to be negative and am just straightforward in general 😅
Thank you, I'll check the playlist and the names out