Re:Programming Languages Going Above and Beyond
by lenkite on Thursday June 29, 2023 @01:51PM
(#36524054)
I wish something like Lamport's TLA+ (https://lamport.azurewebsites.net/tla/tla.html) was supported in modern language compilers - perhaps with annotations/macros and a mini formal DSL.
[ Parent
| on HN ]
Re:Programming Languages Going Above and Beyond
by mrkeen on Thursday June 29, 2023 @02:10PM
(#36524413)
And types too :)
I know many words have been spilled over why it shouldn't have them, but I remain unconvinced.
I modelled a trivial traffic light system to make sure the cars and pedestrians didn't have "green" at the same time. And they didn't, because they had "green_light" at the same time. Oops!
Re:Programming Languages Going Above and Beyond
by abathologist on Thursday June 29, 2023 @02:43PM
(#36524876)
It's still in pretty early development, but you may be interested in https://github.com/informalsystems/quint
> It combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.
And it is typed ;)