I know you all have better things to do with your life but ...
As I've mentioned too many times I'm trying to merge LEAN
proof technology with computer algebra (the SANE project in Axiom).
That involves proving algorithms.
LEAN currently seems more focused on straight math rather than
mathematical algorithms but I'm hoping that will change if we can find
a way toward proving computer algebra programs. This has already
been done with Buchberger's Groebner Basis algorithm in Coq, for example,
which was implemented in Axiom years ago.
One key question is how to abstract software implementations into a
mathematically tractable form suitable for processing by LEAN.
The "crossover" bridge between software algorithms and LEAN seems to
be best captured by Leslie Lamport's TLA+ approach
This rather brief course gives all the needed ideas.
Lamport provides a way to reduce computer algorithms into mathematical
expressions. It seems to me we are one PhD student away from combining
that approach with LEAN to provide a fairly comprehensive proof assistant
capable of handling algorithmic proofs.
The TLA+ machinery combined with the LEAN machinery seems to me
to be a path to including algorithmic proofs in LEAN.
If any of you have a grad student looking for a PhD thesis topic this might
be a useful suggestion. I'm no longer associated with any University so nothing
I do will likely see the light of day.
Tim