Anybody interested, this 2016 paper is a general survey of the current proof logic refinement implementations out there, and the problems and limitations they have which they are currently trying to solve with dependent types/Computational Higher Type Theory http://www.redprl.org/pdfs/afpr.pdf