is automated theorem proving like pure lisps "pltp" really that difficult it came a decade before spark83s ada
another question was theorem proving ever in rusts design https://rust-formal-methods.github.io/tools.html
id say the same about ada but spark has it
and looking at 1-san i doubt he even cares about that in the comparison and in my opinion should drop the spark thing if its for le security probably pick a different language even rust like you said until the second he unsurprisingly enables rusts unsafe mode out of frustration and doesnt use any of the formal method utilities designed around rust