TLA+ should be generated by hand as a extremely detailed spec for LLMs to use to generate code

right? I read the kleppman post sometime ago about formal verification taking off but i could never square away who verifies the verifier.

▲

nextos 5 hours ago | parent [-]

That might emerge as one of the main tasks of future software engineers, writing formal specifications by hand.

It could be the case that Tony Hoare was right, just too early.

▲

twoWhlsGud 2 hours ago | parent [-]

Yes! Formal specs could be where the understanding of what exactly the system is supposed to do gets laid out - and ideally coupled into the verification process that the code produced actually does what it is supposed to (and nothing else...). That would be a big change!

	▲	UltraSane 40 minutes ago \| parent [-]
		It is normal to spend a huge amount of time creating incredibly detailed behavior specs in avionics and other code where people can die from bugs.