Our great sponsors
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model.
C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.
The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].
[1] https://www.microsoft.com/en-us/research/project/code-contra...
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
[4] https://github.com/dafny-lang/dafny
[5] https://github.com/dotnet/csharplang/issues/105
Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model.
C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.
The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].
[1] https://www.microsoft.com/en-us/research/project/code-contra...
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
[4] https://github.com/dafny-lang/dafny
[5] https://github.com/dotnet/csharplang/issues/105
Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model.
C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.
The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].
[1] https://www.microsoft.com/en-us/research/project/code-contra...
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
[4] https://github.com/dafny-lang/dafny
[5] https://github.com/dotnet/csharplang/issues/105
Note that the Z3 SMT solver was written by Leonardo de Moura, who also is the lead dev of Lean 4. Not a coincidence (-;
Lean 4 seems to be used in production at AWS: https://github.com/cedar-policy/cedar-spec/pull/138
Have you looked into Idris2 at all. While looking into these theorum provers, it always felt like they had an impedance mismatch with normal programming.
Idris2 portends to a general purpose language that also has a more advanced type system for the theorum proving.
https://github.com/idris-lang/Idris2
You can even follow his progress on GitHub here:
https://github.com/teorth/symmetric_project/
Yeah, I believe they said intend for it to be used as a general purpose programming language. I used it to complete Advent of Code last year.
There are some really interesting features for general purpose programming in there. For example: you can code updates to arrays in a functional style (change a value, get a new array back), but if the refcount is 1, it updates in place. This works for inductive types and structures, too. So I was able to efficiently use C-style arrays (O(1) update/lookup) while writing functional code. (paper: https://arxiv.org/abs/1908.05647 )
Another interesting feature is that the "do" blocks include mutable variables and for loops (with continue / break / return), that gets compiled down to monad operations. (paper: https://dl.acm.org/doi/10.1145/3547640 )
And I'm impressed that you can add to the syntax of the language, in the same way that the language is implemented, and then use that syntax in the next line of code. (paper: https://lmcs.episciences.org/9362/pdf ). There is an example in the source repository that adds and then uses a JSX-like syntax. (https://github.com/leanprover/lean4/blob/master/tests/playgr... )
There's a list of packages here: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...
Related posts
- If You've Got Enough Money, It's All 'Lawful'
- What are the current hot topics in type theory and static analysis?
- Paper from 2021 claims P=NP with poorly specified algorithm for maximum clique using dynamical systems theory
- Low-level format file of mathlib
- [Hobby] Amateur Generalist Programmer Seeking to Put Bugfixing Skills to Good Use