alt Hacker NewsI 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
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
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.