The Coq mailing list

[Filip Vukovinski <filip.vukovinski AT net.hr>]

Hello from a software engineer,

here are my two cents on the topic,

TLA+ is inspiring and elucidating, but you wouldn't use it in the workspace 
unless you are designing distributed systems or have a process requirement to 
do software verification.

In the latter case, you would prefer a more-mathematical language, that is, a 
language more expressive than your programming language and both TLA+ and Coq 
go that way - Coq being more general: great for new alogirthms and data 
structures as an example.

TLA+ feels more like an update logic, which could be useful for testing 
program behavior, specifically memory use or indeed program complexity or 
even program interaction with the environment. But, compared to Coq, a 
limited tool.

This isn't to say that the Calculus of Constructions is rightly apt to prove 
statements about software...

(There's a great recorded talk by Kevlin Henney about the 6 impossibilities 
in software development, and one of those is exactly about the matter we are 
discussing)

Frankly, I do think more maths knowledge is needed in software dev, but I 
wouldn't go so far as to say that software devs don't know or abhor math - 
they do prefer libraries, but sometimes you do have to write a library or 
indeed, a function (Joy).


Best regards,

Filip Vukovinski 



______________________________________________________________
> Od: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
> Za: "coq-club" <coq-club AT inria.fr>
> Datum: 17.05.2022 19:36
> Naslov: [Coq-Club] Lamport on TLA+ in Quanta, with Coq mention
>
https://www.quantamagazine.org/computing-expert-says-programmers-need-more-math-20220517/

"Coq was designed to do real mathematics and to be able to capture the
reasoning that mathematicians do. ... TLA+ is designed not for
mathematicians but for engineers who want to prove the properties of
their systems. "

IDK.  I do however appreciate his emphasis on improving
"mathematical thinking" instruction for programmers.  But if you manage
to accomplish that, would they not then favor Coq over TLA+ as a
result?  Or, perhaps he is taking a pragmatic stance wrt education: it
won't change, programmers will continue to fear math, so TLA+ it is.