3 ms·

Eiffel, I hear, was (is?) quite cool. I've read some of Bertrand Meyer's work and have learned a lot from it. One area that is becoming really interesting to m

Eiffel, I hear, was (is?) quite cool. I've read some of Bertrand Meyer's work and have learned a lot from it. One area that is becoming really interesting to me is in dependently typed languages and their ability to encode at least some of the properties of the formal specification in the type system. I haven't had much time to take a deep dive into Agda but what I have challenged myself with gives me hope that this may be the way we write programs in the future (even if it's not Agda per se).

nickpsecurity 10y ago
Re meyer The neat thing is his method was adopted commercially with years of success despite never showing up on Hacker News, etc. It combined efficiency, OOP, basic safety, and concurrency safety (SCOOP). Most talk about adoption of formal specs in theory but he got it done in practice with DbC in industry. Now, tools like SPARK, Ada 2012, and Perfect Developer are using it. You can do it in C, C# and Java, too. Btw, in case you missed it, his Theory of Programs defines most aspects of programming in an elegant, precise way using set theory: https://arxiv.org/pdf/1507.00723v3 https://arxiv.org/pdf/1507.00723v3 Re dependent Learn from the master: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ Far as whether they're good, Im not sure as formal methodists have endless arguments on it. The critics basically say you have to put in enough spec and proving work that you might as well do the real thing in a prover then extract it. Chlipala actually does something like that called Programs as Proofs I think. Memory gettimg fuzzy. Just remember dependent types vs proving is in dispute at the moment.