I think it is even more relevant today.

Hoare Logic + Dijkstra's weakest precondition + Meyer's Design-by-Contract is what should be used to get LLMs to generate proof with code in a correctness-by-construction approach to implementation.

References:

Correctness-by-Construction (CbC) - https://www.tu-braunschweig.de/en/isf/research/cbc

A Course on Correctness by Construction - https://wp.software.imdea.org/cbc/