interactive VS dafny

All of this will be accomplished inside of a single Polyglot Notebook. If you're not familiar with Polyglot Notebooks, they're a technology built on top of Jupyter Notebooks that allow you to use additional language kernels, including a F# Kernel. This lets you run interactive data science experiments in a single notebook as shown here in VS Code:

I use .NET on Linux and the experience with Rider has been great. The workflow transfers really well between Mac, Windows, and Linux, and everything works the way you expect. The only problems I run into are that there are still things that are Windows focused. For example MAUI does not run on Linux which is a shame because we could use another cross platform GUI.

There are still bugs, for example I ran into one with Polyglot Notebooks not working on Manjaro or Pop!_OS https://github.com/dotnet/interactive/issues/3159

First of all, if you have a small amount of code that lives in an individual C# file and you wanted to reference it in your notebook, you can do this via the #!import magic command as shown below:

My 2 cents: use a Personal Access Token instead of a password, it is much safer (even though not 100% safe). Some references: https://github.com/dotnet/interactive/discussions/1340 https://learn.microsoft.com/en-us/azure/devops/organizations/accounts/use-personal-access-tokens-to-authenticate

See also https://github.com/dotnet/interactive

U have Powershell notebooks https://github.com/dotnet/interactive

Or Rider or simply install dotnet by itself (very easy) and code in a notepad or VSCode. .NET interactive is another awesome way to start: https://github.com/dotnet/interactive/blob/main/docs/display-output-csharp.md

Hi! My name is Claudia and I am a PM at Microsoft (opinions are my own) working on Polyglot Notebooks in VS Code. Polyglot Notebooks are exactly what you are describing! They are notebooks where you can use multiple languages AND share variables between them to ensure a continuous workflow. Not only that, but each language has language server support. Polyglot Notebooks currently supports C#, F#, PowerShell, JavaScript, HTML, SQL, KQL, and Mermaid.

We have just added support for Python and R integration and I am actually in search of external testers! If you are willing to sign an NDA to try out our Python and R integration and give us feedback please drop your email in the form below and I will reach out with instructions for you to try it out!

https://forms.office.com/r/UQchfQSGa5

If you'd like to start trying it out today you can install the extension from the marketplace here: https://marketplace.visualstudio.com/items?itemName=ms-dotne...

https://github.com/dotnet/interactive

I've been excited about a lot of the work being done in .NET Interactive and Polyglot Notebooks, particuarly with ML with F#. I don't know too much about ML, so I thought I'd check out ML.NET.

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

I don't think something that specific exists. There are a very large number of formal methods tools, each with different specialties / domains.

For verification with proof assistants, [Software Foundations](https://softwarefoundations.cis.upenn.edu/) and [Concrete Semantics](http://concrete-semantics.org/) are both solid.

For verification via model checking, you can check out [Learn TLA+](https://learntla.com/), and the more theoretical [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf).

For more theory, check out [Formal Reasoning About Programs](http://adam.chlipala.net/frap/).

And for general projects look at [F*](https://www.fstar-lang.org/) and [Dafny](https://dafny.org/).

Dafny and Whiley are two examples with explicit verification support. Idris and other dependently typed languages should all be rich enough to express the required predicate but might not necessarily be able to accept a reasonable implementation as proof. Isabelle, Lean, Coq, and other theorem provers definitely can express the capability but aren't going to churn out much in the way of executable programs; they're more useful to guide an implementation in a more practical functional language but then the proof is separated from the implementation, and you could also use tools like TLA+.

https://dafny.org/

https://whiley.org/

https://www.idris-lang.org/

https://isabelle.in.tum.de/

https://leanprover.github.io/

https://coq.inria.fr/

http://lamport.azurewebsites.net/tla/tla.html

> I think we can assume it won't be as efficient has hand written code

Actually, surprisingly, not necessarily the case!

If you'll refer to the discussion in https://github.com/dafny-lang/dafny/issues/601 and in https://github.com/dafny-lang/dafny/issues/547, Dafny can statically prove that certain compiler branches are not possible and will never be taken (such as out-of-bounds on index access, logical assumptions about whether a value is greater than or less than some other value, etc). This lets you code in the assumptions (__assume in C++ or unreachable_unchecked() under rust) that will allow the compiler to optimize the codegen using this information.

Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.

I'm not sure if the author is here, or if my comment attempt was successful. So, can I suggest you take a look at a third leg of the formal methods stool?

If you are familiar with C, check out Frama-C (https://frama-c.com/) and the WP and RTE plugins. The approach is based on Tony Hoare and EWD's axiomatic semantics (https://en.wikipedia.org/wiki/Hoare_logic). It does not have a good memory management story, as far as I know, but is very good for demonstrating value correctness (RTE automatically generates assertions for numeric runtime errors, for example) and many memory errors.

If you are familiar with Ada, check out SPARK (https://www.adacore.com/about-spark), which is similar to Frama-C but has a much better interface in the AdaCore GNAT toolkit and IDE.

Both work similarly: Assertions in normal Ada or C code as well as the code itself are translated into SMT statements and fed to a SMT solver to find counterexamples---errors.

I have some blog posts from several years ago about Frama-C:https://maniagnosis.crsr.net/tags/applied%20formal%20logic.h... (And I really should get back into it; it's a lot of fun.)

If you are not familiar with Ada or C, Dafny (https://dafny.org/) is another option based on .NET and devoleped at Microsoft. It seems nigh-on perfect for this approach. (The language uses a garbage collector.) At the time I was looking, there was little documentation on Dafny, but that seems to have improved.