I predict in 10 years „code“ that is not actually in the language of a proof assistant will be the exception, not the norm. This will happen by proof assistant languages becoming easier to the point that normal code will look cumbersome

▲

pydry 2 days ago | parent [-]

Back when I first studied this 20 years ago the progenitors predicted it would get very popular one day.

What actually happened was that some programming languages borrowed a few concepts and life carried on as before.

	▲	auggierose a day ago \| parent [-]
		I started with this 30 years ago, so yeah, I know the history :-) This time is different.