Version 8.12 har slÀppts (den senaste tillgÀngliga minor versionen vid tidpunkten för denna nyhet Àr 8.12.1) av verktyget för interaktiv bevisföring av satser Coq (höna).
Coq innehÄller programmeringssprÄket med beroende typer Gallina (kyckling), som bygger pÄ teorin om konstruktioner.
Systemet Coq möjliggör utveckling av bÄde datorverifierade bevis av satser och program tillsammans med bevis för överensstÀmmelse med specifikationen.
I den nya versionen har standardbiblioteket och dokumentationen genomgÄtt betydande förbÀttringar, och ett antal buggar har ÄtgÀrdats.
KĂ€lla: linux.org.ru
