Π’Ρ‹ΡˆΠ»Π° вСрсия 8.12 (послСдняя доступная минорная вСрсия Π½Π° ΠΌΠΎΠΌΠ΅Π½Ρ‚ написания новости – 8.12.1) инструмСнта ΠΈΠ½Ρ‚Π΅Ρ€Π°ΠΊΡ‚ΠΈΠ²Π½ΠΎΠ³ΠΎ Π΄ΠΎΠΊΠ°Π·Π°Ρ‚Π΅Π»ΡŒΡΡ‚Π²Π° Ρ‚Π΅ΠΎΡ€Π΅ΠΌ Coq (ΠΏΠ΅Ρ‚ΡƒΡˆΠΎΠΊ).

Coq Π²ΠΊΠ»ΡŽΡ‡Π°Π΅Ρ‚ Π² сСбя язык программирования с зависимыми Ρ‚ΠΈΠΏΠ°ΠΌΠΈ Gallina (ΠΊΡƒΡ€ΠΈΡ†Π°), ΠΎΠΏΠΈΡ€Π°ΡŽΡ‰ΠΈΠΉΡΡ Π½Π° Ρ‚Π΅ΠΎΡ€ΠΈΡŽ исчислСния конструкций.

БистСма Coq позволяСт Ρ€Π°Π·Ρ€Π°Π±Π°Ρ‚Ρ‹Π²Π°Ρ‚ΡŒ ΠΊΠ°ΠΊ ΠΊΠΎΠΌΠΏΡŒΡŽΡ‚Π΅Ρ€Π½ΠΎ-Π²Π΅Ρ€ΠΈΡ„ΠΈΡ†ΠΈΡ€ΡƒΠ΅ΠΌΡ‹Π΅ Π΄ΠΎΠΊΠ°Π·Π°Ρ‚Π΅Π»ΡŒΡΡ‚Π²Π° Ρ‚Π΅ΠΎΡ€Π΅ΠΌ, Ρ‚Π°ΠΊ ΠΈ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΡ‹ вмСстС с Π΄ΠΎΠΊΠ°Π·Π°Ρ‚Π΅Π»ΡŒΡΡ‚Π²ΠΎΠΌ соотвСтствия спСцификации.

Π’ Π½ΠΎΠ²ΠΎΠΉ вСрсии Π±Ρ‹Π»Π° Π·Π½Π°Ρ‡ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ Π΄ΠΎΡ€Π°Π±ΠΎΡ‚Π°Π½Π° стандартная Π±ΠΈΠ±Π»ΠΈΠΎΡ‚Π΅ΠΊΠ° ΠΈ докумСнтация, Π° Ρ‚Π°ΠΊΠΆΠ΅ исправлСн ряд ошибок.

Π˜ΡΡ‚ΠΎΡ‡Π½ΠΈΠΊ: linux.org.ru