I'm a big fan of the various "gradual" approaches so this paper really caught my eye. Gradualizing the Calculus of Inductive Constructions (https://hal.archive

I'm a big fan of the various "gradual" approaches so this paper really caught my eye. Gradualizing the Calculus of Inductive Constructions (https://hal.archives-ouvertes.fr/hal-02896776/ https://hal.archives-ouvertes.fr/hal-02896776/) I'm not sure if this is precisely the direction things should go in order to improve the utilisation of specification within software development but it's a very important contribution. As yet my favourite development style has been with F-star but F-star also leaves me a bit in a lurch when the automatic system isn't able to find the answer. Too much hinting in the case of hard proofs. Eventually there will be a system that lets you turn the crank up on specification late in the game, allows lots of the assertions to be discharged automatically, and then finally saddles you with the remaining proof obligations in a powerful proof assistant.